{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation   #-}

module Agda.TypeChecking.Rules.Record where

import Prelude hiding (null, not, (&&), (||))

import Data.Maybe
import qualified Data.Set as Set

import Agda.Interaction.Options

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

import Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
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.CompiledClause (hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.InstanceArguments

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

import Agda.Utils.Boolean
import Agda.Utils.Function ( applyWhen )
import Agda.Utils.Lens
import Agda.Utils.List (headWithDefault)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.POMonoid
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Size

import Agda.Utils.Impossible

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

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

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

  traceCall (CheckRecDef (getRange name) name ps fields) $ do
    reportSDoc "tc.rec" 10 $ vcat
      [ "checking record def" <+> prettyTCM name
      , nest 2 $ "ps ="     <+> prettyList (map prettyA ps)
      , nest 2 $ "contel =" <+> prettyA contel
      , nest 2 $ "fields =" <+> prettyA (map Constr fields)
      ]
    -- get type of record
    def <- instantiateDef =<< getConstInfo name
    t   <- instantiateFull $ defType def
    let npars =
          case Definition -> Defn
theDef Definition
def of
            DataOrRecSig Nat
n -> Nat
n
            Defn
_              -> Nat
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- If the record type is erased, then hard compile-time mode is
    -- entered.
    setHardCompileTimeModeIfErased' def $ do

    parNames <- getGeneralizedParameters gpars name

    bindGeneralizedParameters parNames t $ \ Telescope
gtel Type
t0 ->
     Nat
-> [LamBinding] -> Type -> (Telescope -> Type -> TCM ()) -> TCM ()
forall a.
Nat
-> [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameters (Nat
npars Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [Maybe Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
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.
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking fields"
      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
      reportSDoc "tc.rec" 20 $ vcat
        [ "contype = " <+> prettyTCM contype ]

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

      -- Compute correct type of constructor

      -- t = tel -> t0 where t0 must be a sort s
      TelV idxTel s <- telView t0
      unless (null idxTel) $ typeError $ ShouldBeASort t0
      s <- forceSort s

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

      reportSDoc "tc.rec" 20 $ do
        gamma <- getContextTelescope  -- the record params (incl. module params)
        "gamma = " <+> inTopContext (prettyTCM gamma)

      -- record type (name applied to parameters)
      rect <- El s . Def name . map Apply <$> 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 = Telescope -> Type -> Type
telePi_ Telescope
ftel (Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ftel) Type
rect)
        -- NB: contype does not contain the parameter telescope

      -- Obtain name of constructor (if present).
      (hasNamedCon, conName) <- case con of
        A.NamedRecCon QName
c -> (Bool, QName) -> TCMT IO (Bool, QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, QName
c)
        A.FreshRecCon QName
c -> (Bool, QName) -> TCMT IO (Bool, QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, QName
c)

      -- Add record type to signature.
      reportSDoc "tc.rec" 15 $ "adding record type to signature"

      etaenabled <- etaEnabled

      let getName :: A.Declaration -> [Dom QName]
          getName (A.Field DefInfo
_ QName
x Arg Expr
arg)    = [QName
x QName -> Dom' Term Expr -> Dom' Term QName
forall a b. a -> Dom' Term b -> Dom' Term a
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' Term QName]
getName Field
f
          getName Field
_                    = []

          setTactic Dom' t e
dom Dom' t e
f = Dom' t e
f { domTactic = domTactic dom }

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

          -- indCo is what the user wrote: inductive/coinductive/Nothing.
          -- We drop the Range.
          indCo = 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 -> 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.
          noEta    = HasEta -> EtaEquality
Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta
forall a. a -> HasEta' a
NoEta PatternOrCopattern
patCopat
          haveEta0 = EtaEquality
-> (HasEta -> EtaEquality) -> Maybe HasEta -> EtaEquality
forall b a. b -> (a -> b) -> Maybe a -> b
maybe EtaEquality
noEta HasEta -> EtaEquality
Specified Maybe HasEta
eta
          con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
conName (PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
patCopat) Induction
conInduction ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
forall a b. (a -> b) -> a -> b
$ (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs

          -- A record is irrelevant if all of its fields are.
          -- In this case, the associated module parameter will be irrelevant.
          -- See issue #392.
          -- Unless it's been declared coinductive or no-eta-equality (#2607).
          recordRelevance
            | Just NoEta{} <- Maybe HasEta
eta         = Relevance
relevant
            | Induction
CoInductive <- Induction
conInduction = Relevance
relevant
            | [Dom ([Char], Type)] -> Bool
forall a. Null a => a -> Bool
null (Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel)       = Relevance
relevant    -- #6270: eta unit types don't need to be irrelevant
            | Bool
otherwise                   = [Relevance] -> Relevance
forall a. Ord a => [a] -> a
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 ([Char], Type) -> Relevance)
-> [Dom ([Char], Type)] -> [Relevance]
forall a b. (a -> b) -> [a] -> [b]
map Dom ([Char], Type) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel)

      -- Andreas, 2017-01-26, issue #2436
      -- Disallow coinductive records with eta-equality
      -- Andreas, 2024-06-14, PR #7300
      -- Just make this a deadcode warning.
      haveEta <-
        if (conInduction == CoInductive && theEtaEquality haveEta0 == YesEta) then do
          noEta <$ do
            setCurrentRange eta0 $ warning $ CoinductiveEtaRecord name
        else pure haveEta0
      reportSDoc "tc.rec" 30 $ "record constructor is " <+> prettyTCM con

      -- Jesper, 2021-05-26: Warn when declaring coinductive record
      -- but neither --guardedness nor --sized-types is enabled.
      when (conInduction == CoInductive) $ do
        unlessM ((optGuardedness || optSizedTypes) <$> pragmaOptions) $
          warning $ NoGuardednessFlag 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 = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
          telh  = (Dom Type -> Dom Type) -> Telescope -> Telescope
forall a b. (a -> b) -> Tele a -> Tele b
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
      escapeContext impossible npars $ do
        addConstant' name defaultArgInfo t $
            Record
              { recPars           = npars
              , recClause         = Nothing
              , recConHead        = con
              , recNamedCon       = hasNamedCon
              , recFields         = fs
              , recTel            = telh `abstract` ftel
              , recAbstr          = Info.defAbstract i
              , recEtaEquality'   = haveEta
              , recPatternMatching= patCopat
              , recInduction      = indCo
                  -- We retain the original user declaration [(co)inductive]
                  -- in case the record turns out to be recursive.
              -- Determined by positivity checker:
              , recMutual         = Nothing
              -- Determined by the termination checker:
              , recTerminates     = Nothing
              , recComp           = emptyCompKit -- filled in later
              }

        erasure <- optErasure <$> pragmaOptions
        -- Add record constructor to signature
        addConstant' conName defaultArgInfo
             -- If --erasure is used, then the parameters are erased
             -- in the constructor's type.
            (applyWhen erasure (fmap $ applyQuantity zeroQuantity) telh
             `abstract` contype) $
            Constructor
              { conPars   = npars
              , conArity  = size fs
              , conSrcCon = con
              , conData   = name
              , conAbstr  = Info.defAbstract i
              , conComp   = emptyCompKit  -- filled in later
              , conProj   = Nothing       -- filled in later
              , conForced = []
              , conErased = Nothing
              , conErasure = erasure
              , conInline  = False
              }

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

      -- Check that the fields fit inside the sort
      _ <- fitsIn conName uc [] contype s

      -- Check that the sort admits record declarations.
      checkDataSort name 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 = Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
recordRelevance ArgInfo
defaultArgInfo
          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 = QName -> ModuleName
qnameToMName QName
name  -- Name of record module.

      eraseRecordParameters <- optEraseRecordParameters <$> pragmaOptions
      let maybeErase :: forall a. LensQuantity a => a -> a
          maybeErase | Bool
eraseRecordParameters = Quantity -> a -> a
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity
                     | Bool
otherwise             = a -> a
forall a. a -> a
id

      -- Andreas, 2016-02-09 setting all parameters hidden in the record
      -- section telescope changes the semantics, see e.g.
      -- test/Succeed/RecordInParModule.
      -- Ulf, 2016-03-02 but it's the right thing to do (#1759)
      modifyContextInfo (hideOrKeepInstance . maybeErase) $ addRecordVar $ do

        -- Add the record section.

        reportSDoc "tc.rec.def" 10 $ sep
          [ "record section:"
          , nest 2 $ sep
            [ prettyTCM m <+> (inTopContext . prettyTCM =<< getContextTelescope)
            , fsep $ punctuate comma $ map (return . P.pretty . map argFromDom . getName) fields
            ]
          ]
        reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat
          [ "field tel =" <+> escapeContext impossible 1 (prettyTCM ftel)
          ]
        addSection 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.
      modifyContextInfo (hideOrKeepInstance . maybeErase) $ do
        -- If --erasure is used, then the parameters are erased in the
        -- types of the projections.
        erasure <- optErasure <$> pragmaOptions
        params  <- applyWhen erasure (fmap $ applyQuantity zeroQuantity) <$> getContext

        -- Check the types of the fields and the other record declarations.
        addRecordVar $ withCurrentModule m $ 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.
          tel' <- do
            r <- headWithDefault __IMPOSSIBLE__ <$> getContext
            return $ contextToTel $ r : params
          setModuleCheckpoint m
          checkRecordProjections m name hasNamedCon con tel' ftel fields


      -- we define composition here so that the projections are already in the signature.
      whenM cubicalCompatibleOption do
        escapeContext impossible npars do
          addCompositionForRecord name haveEta con tel (map argFromDom fs) ftel rect

      -- The confluence checker needs to know what symbols match against
      -- the constructor.
      modifySignature $ updateDefinition conName $ \Definition
def ->
        Definition
def { defMatchable = Set.fromList $ map unDom fs }

  where
  -- Andreas, 2020-04-19, issue #4560
  -- If the user declared the record constructor as @pattern@,
  -- then switch on pattern matching for no-eta-equality.
  -- Default is no pattern matching, but definition by copatterns instead.
  patCopat :: PatternOrCopattern
patCopat = 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 a b. a -> HasEta' b -> HasEta' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (HasEta0 -> HasEta)
-> (Ranged HasEta0 -> HasEta0) -> Ranged HasEta0 -> HasEta
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged HasEta0 -> HasEta0
forall a. Ranged a -> a
rangedThing) (Ranged HasEta0 -> HasEta)
-> Maybe (Ranged HasEta0) -> Maybe HasEta
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged HasEta0)
eta0


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

    -- Record has no fields: attach composition data to record constructor
    if null fs then do
      kit <- defineCompData name con (abstract cxt tel) [] ftel rect []
      modifySignature $ updateDefinition (conName con) $ updateTheDef $ \case
        r :: Defn
r@Constructor{} -> Defn
r { conComp = kit, conProj = Just [] }  -- no projections
        Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- No-eta record with pattern matching (i.e., withOUT copattern
    -- matching): define composition as for a data type, attach it to
    -- the record.
    else if theEtaEquality eta == NoEta PatternMatching then do
      kit <- defineCompData name con (abstract cxt tel) (unArg <$> fs) ftel rect []
      modifySignature $ updateDefinition name $ updateTheDef $ \case
        r :: Defn
r@Record{} -> Defn
r { recComp = kit }
        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.
      kit <- ifM (return (any isIrrelevant fs)
                  `and2M` do not . optIrrelevantProjections <$> pragmaOptions)
        {-then-} (return emptyCompKit)
        {-else-} (defineCompKitR name (abstract cxt tel) ftel fs rect)
      modifySignature $ updateDefinition name $ updateTheDef $ \case
        r :: Defn
r@Record{} -> Defn
r { recComp = 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
  required <- (SomeBuiltin -> TCMT IO (Maybe Term))
-> [SomeBuiltin] -> TCMT IO [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SomeBuiltin -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm'
        [ BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinInterval
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinIZero
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinIOne
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinIMin
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinIMax
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinINeg
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinPOr
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinItIsOne
        ]
  reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
  reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
  reportSDoc "tc.rec.cxt" 30 $ pretty rect
  if not $ all isJust required then return $ emptyCompKit else do
    transp <- whenDefined [builtinTrans]              (defineKanOperationR DoTransp name params fsT fns rect)
    hcomp  <- whenDefined [builtinTrans,builtinHComp] (defineKanOperationR DoHComp name params fsT fns rect)
    return $ CompKit
      { nameOfTransp = transp
      , nameOfHComp  = hcomp
      }
  where
    whenDefined :: t a -> m (Maybe a) -> m (Maybe a)
whenDefined t a
xs m (Maybe a)
m = do
      xs <- (a -> m (Maybe Term)) -> t a -> m (t (Maybe Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM a -> m (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' t a
xs
      if all isJust xs then m else return Nothing


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

  caseMaybe stuff (return Nothing) $ \ (QName
theName, Telescope
gamma, Type
rtype, [Dom Type]
clause_types, [Term]
bodies) -> do
  -- phi = 1 clause
  c' <- do
           io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
           Just io_name <- getBuiltinName' builtinIOne
           one <- primItIsOne
           tInterval <- primIntervalType
           let
              (ix,rhs) =
                case cmd of
                  -- TranspRArgs = phi : I, a0 : ..
                  -- Γ = Δ^I , CompRArgs
                  -- pats = ... | phi = i1
                  -- body = a0
                  Command
DoTransp -> (Nat
1,Nat -> Elims -> Term
Var Nat
0 [])
                  -- HCompRArgs = phi : I, u : .., a0 : ..
                  -- Γ = Δ, CompRArgs
                  -- pats = ... | phi = i1
                  -- body = u i1 itIsOne
                  Command
DoHComp  -> (Nat
2,Nat -> Elims -> Term
Var Nat
1 [] 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 = 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
forall p. DataOrRecord' p
IsData Induction
Inductive [])
                       (ConPatternInfo
noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
                                         , conPFallThrough = True })
                         []

              -- gamma, rtype

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

              pats :: [NamedArg DeBruijnPattern]
              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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma

              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' = [[Char]] -> [Dom Type] -> Telescope
unflattenTel ([[Char]]
ns0 [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
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) = Nat -> [Dom Type] -> ([Dom Type], [Dom Type])
forall a. Nat -> [a] -> ([a], [a])
splitAt (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
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
                ([[Char]]
ns0,[Char]
_:[[Char]]
ns1) = Nat -> [[Char]] -> ([[Char]], [[Char]])
forall a. Nat -> [a] -> ([a], [a])
splitAt (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
ix) ([[Char]] -> ([[Char]], [[Char]]))
-> [[Char]] -> ([[Char]], [[Char]])
forall a b. (a -> b) -> a -> b
$ Telescope -> [[Char]]
teleNames Telescope
gamma

              c = Clause { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseTel :: Telescope
clauseTel       = Telescope
gamma'
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , 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
                         , 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
                         , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                         , 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
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                         }
           reportSDoc "trans.rec.face" 17 $ text $ show c
           return c
  cs <- forM (zip3 fns clause_types bodies) $ \ (Arg QName
fname, Dom Type
clause_ty, Term
body) -> do
          let
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [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 { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseTel :: Telescope
clauseTel       = Telescope
gamma
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
body
                         , 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)
                         , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                         , 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
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                         }
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
17 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Clause -> [Char]
forall a. Show a => a -> [Char]
show Clause
c
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
16 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"type =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Maybe (Arg Type) -> [Char]
forall a. Show a => a -> [Char]
show (Clause -> Maybe (Arg Type)
clauseType Clause
c))
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> TCMT IO Doc) -> Type -> TCMT IO 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)
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"body =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma Term
body)
          Clause -> TCMT IO Clause
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  addClauses theName $ c' : cs
  reportSDoc "trans.rec" 15 $ text $ "compiling clauses for " ++ show theName
  (mst, _, cc) <- inTopContext (compileClauses Nothing cs)
  whenJust mst $ setSplitTree theName
  setCompiledClauses theName cc
  reportSDoc "trans.rec" 15 $ text $ "compiled"
  return $ Just 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 (perhaps erased) and record variable r ("self")

    [@ftel@ ]  telescope of fields

    [@fs@   ]  the fields to be checked
-}
checkRecordProjections ::
  ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
  [A.Declaration] -> TCM ()
checkRecordProjections :: ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Field]
-> TCM ()
checkRecordProjections ModuleName
m QName
r Bool
hasNamedCon ConHead
con Telescope
tel Telescope
ftel [Field]
fs = do
    Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs 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 a. a -> TCMT IO a
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 a b. TCMT IO a -> TCMT IO b -> TCMT IO b
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 a. Call -> TCMT IO a -> TCMT IO a
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.
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking projection" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"top   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope)
          , TCMT IO Doc
"tel   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO 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...
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ftel1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Nat
1 (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
ftel1)
          , TCMT IO Doc
"t     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Nat
1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
ftel1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t)
          , TCMT IO Doc
"ftel2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Nat
1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
ftel1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Dom Type
-> Abs Telescope -> (Telescope -> TCMT IO Doc) -> TCMT IO 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM)
          ]
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
55 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ftel1 (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
ftel1
          , TCMT IO Doc
"t     (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
          , TCMT IO Doc
"ftel2 (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Telescope
ftel2
          ]
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"vs    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM [Term]
vs)
          , TCMT IO Doc
"abstr =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (IsAbstract -> [Char]) -> IsAbstract -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> [Char]
forall a. Show a => a -> [Char]
show) (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
info)
          , TCMT IO Doc
"quant =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Quantity -> [Char]) -> Quantity -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> [Char]
forall a. Show a => a -> [Char]
show) (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai)
          , TCMT IO Doc
"coh   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Cohesion -> [Char]) -> Cohesion -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cohesion -> [Char]
forall a. Show a => a -> [Char]
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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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 TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Cohesion -> TypeError
InvalidFieldModality (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

      -- For now, we forbid any polarity annotations on record fields (we would need to do as above,
      -- and eta-equality or projection existence would be in danger).
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
ai PolarityModality -> PolarityModality -> Bool
`samePolarity` (ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
MixedPolarity)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        [Char] -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot have record field with " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PolarityModality -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
ai) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" polarity"

      -- 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'       = Nat -> Nat -> Type -> Type
forall a. Subst a => Nat -> Nat -> a -> a
raiseFrom (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ftel1) Nat
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 ([Char] -> Telescope -> Telescope
forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
"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 = Nat -> Elims -> Term
Var Nat
0 [ProjOrigin -> QName -> Elim
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
$ [Char] -> Telescope -> Abs Telescope
forall a. [Char] -> a -> Abs a
Abs (Name -> [Char]
nameToArgName (Name -> [Char]) -> Name -> [Char]
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

      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"finalt=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"adding projection"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
projname TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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 = Bool -> (Term -> Term) -> Term -> Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel) Term -> Term
dontCare

        let -- Andreas, 2010-09-09: comment for existing code
            -- split the telescope into parameters (ptel) and the type or the record
            -- (rt) which should be  R ptel
            telList :: [Dom ([Char], Type)]
telList = Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
            ([Dom ([Char], Type)]
ptelList,[Dom ([Char], Type)
rt]) = Nat
-> [Dom ([Char], Type)]
-> ([Dom ([Char], Type)], [Dom ([Char], Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) [Dom ([Char], Type)]
telList
            ptel :: Telescope
ptel   = [Dom ([Char], Type)] -> Telescope
telFromList [Dom ([Char], Type)]
ptelList
            cpo :: PatOrigin
cpo    = if Bool
hasNamedCon then PatOrigin
PatOCon else PatOrigin
PatORec
            cpi :: ConPatternInfo
cpi    = ConPatternInfo { conPInfo :: PatternInfo
conPInfo   = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
cpo []
                                    , conPRecord :: Bool
conPRecord = Bool
True
                                    , conPFallThrough :: Bool
conPFallThrough = Bool
False
                                    , conPType :: Maybe (Arg Type)
conPType   = 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
$ (([Char], Type) -> Type) -> Dom ([Char], Type) -> Dom Type
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> Type
forall a b. (a, b) -> b
snd Dom ([Char], 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 t. DeBruijn a => Tele (Dom t) -> [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
$ Nat -> Term
var (Abs Telescope -> Nat
forall a. Sized a => a -> Nat
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
$ Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Abs Telescope -> Nat
forall a. Sized a => a -> Nat
size Abs Telescope
ftel2) Type
t
            clause :: Clause
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
                            , 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
                            , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                            }

        let projection :: Projection
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 :: Nat
projIndex    = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel -- which is @size ptel + 1@
              , projLams :: ProjLams
projLams     = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> Arg [Char])
-> [Dom ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term [Char] -> Arg [Char])
-> (Dom ([Char], Type) -> Dom' Term [Char])
-> Dom ([Char], Type)
-> Arg [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Type) -> [Char])
-> Dom ([Char], Type) -> Dom' Term [Char]
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst) [Dom ([Char], Type)]
telList
              }

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

        reportSDoc "tc.cc" 60 $ do
          sep [ "compiled clauses of " <+> prettyTCM projname
              , nest 2 $ text (show cc)
              ]

        escapeContext impossible (size tel) $ do
          lang <- getLanguage
          fun  <- emptyFunctionData
          let -- It should be fine to mark a field with @ω in an
              -- erased record type: the field will be non-erased, but
              -- the projection will be erased. The following code
              -- ensures that the use of addConstant does not trigger
              -- a PlentyInHardCompileTimeMode warning.
              ai' = ((Quantity -> Quantity) -> ArgInfo -> ArgInfo)
-> ArgInfo -> (Quantity -> Quantity) -> ArgInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Quantity -> Quantity) -> ArgInfo -> ArgInfo
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity ArgInfo
ai ((Quantity -> Quantity) -> ArgInfo)
-> (Quantity -> Quantity) -> ArgInfo
forall a b. (a -> b) -> a -> b
$ \case
                      Quantityω QωOrigin
_ -> QωOrigin -> Quantity
Quantityω QωOrigin
QωInferred
                      Quantity
q           -> Quantity
q
          addConstant projname $
            (defaultDefn ai' projname (killRange finalt) lang $ FunctionDefn $
             set funProj_ True $
              fun
                { _funClauses        = [clause]
                , _funCompiled       = Just cc
                , _funSplitTree      = mst
                , _funProjection     = Right projection
                , _funMutual         = Just []  -- Projections are not mutually recursive with anything
                , _funTerminates     = Just True
                })
              { defArgOccurrences = [StrictPos]
              , defCopatternLHS   = hasProjectionPatterns cc
              }
          computePolarity [projname]

        addContext ftel1 case Info.defInstance info of
          -- Instance projections have to be added with their types "qua
          -- local variable" (i.e. the type you'd get were you to open
          -- the record module), but this type has to be treated in the
          -- context ftel1 otherwise it's nonsense
          InstanceDef KwRange
_r -> QName -> Type -> TCM ()
addTypedInstance QName
projname Type
t
          IsInstance
NotInstanceDef -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        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