{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation   #-}

module Mikan.TypeChecking.Rules.Record where

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

import Data.Maybe

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

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Positivity.Occurrence
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Polarity
import Mikan.TypeChecking.Warnings
import Mikan.TypeChecking.CompiledClause (hasProjectionPatterns)
import Mikan.TypeChecking.CompiledClause.Compile
import Mikan.TypeChecking.InstanceArguments
import Mikan.TypeChecking.Rules.Record.Cubical (addCompositionForRecord)

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

import Mikan.Utils.Boolean
import Mikan.Utils.List
import Mikan.Utils.List1 (pattern (:|) )
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Utils.Size

import Mikan.Utils.Impossible
import Mikan.Utils.List1 qualified as List1

---------------------------------------------------------------------------
-- * 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.
  -> PositivityCheck           -- ^ Report positivity errors for this record type?
  -> 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
-> PositivityCheck
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> TCM ()
checkRecDef DefInfo
i QName
name PositivityCheck
pc 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 [Declaration]
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 Type (builtinType) 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
builtinType
  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__

    parNames <- getGeneralizedParameters gpars name

    bindGeneralizedParameters parNames t $ \ Telescope
gtel Type
t0 ->
     DataOrRecord
-> Nat
-> [LamBinding]
-> Type
-> (Telescope -> Type -> TCM ())
-> TCM ()
forall a.
DataOrRecord
-> Nat
-> [LamBinding]
-> Type
-> (Telescope -> Type -> TCM a)
-> TCM a
bindParameters (PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
patCopat) (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.
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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, 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 = \case
            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 t. Arg a -> Dom' t a
domFromArg Arg Expr
arg ]
            A.ScopedDecl ScopeInfo
_ (Declaration
f :| []) -> Declaration -> [Dom' Term QName]
getName Declaration
f
            Declaration
_ -> []

          setTactic Dom' t e
dom Dom' t e
f = Dom' t e
f Dom' t e -> (Dom' t e -> Dom' t e) -> Dom' t e
forall a b. a -> (a -> b) -> b
& (Maybe t -> Identity (Maybe t)) -> Dom' t e -> Identity (Dom' t e)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic ((Maybe t -> Identity (Maybe t))
 -> Dom' t e -> Identity (Dom' t e))
-> Maybe t -> Dom' t e -> Dom' t e
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Dom' t e
dom Dom' t e -> Getting (Maybe t) (Dom' t e) (Maybe t) -> Maybe t
forall s a. s -> Getting a s a -> a
^. Getting (Maybe t) (Dom' t e) (Maybe t)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic)
          fs = (Dom' Term (ArgName, Type) -> Dom' Term QName -> Dom' Term QName)
-> [Dom' Term (ArgName, Type)]
-> [Dom' Term QName]
-> [Dom' Term QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Dom' Term (ArgName, Type) -> Dom' Term QName -> Dom' Term QName
forall {t} {e} {e}. Dom' t e -> Dom' t e -> Dom' t e
setTactic (Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
ftel) ([Dom' Term QName] -> [Dom' Term QName])
-> [Dom' Term QName] -> [Dom' Term QName]
forall a b. (a -> b) -> a -> b
$ (Declaration -> [Dom' Term QName])
-> [Declaration] -> [Dom' Term QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Declaration -> [Dom' Term QName]
getName [Declaration]
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 -> [QName] -> ConHead
ConHead QName
conName (PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
patCopat) Induction
conInduction ([QName] -> ConHead) -> [QName] -> ConHead
forall a b. (a -> b) -> a -> b
$ (Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom [Dom' Term QName]
fs

      -- 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

      -- 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 => a -> a
hideExplicit 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
              , recPositivityCheck= pc
              , 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 (analysis running always, independently of recPositivityCheck):
              , recMutual         = Nothing
              -- Determined by the termination checker:
              , recTerminates     = Nothing
              , recComp           = emptyCompKit -- filled in later
              }

        -- Add record constructor to signature
        addConstant' conName defaultArgInfo
            (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 = []
              , 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.
          KwRange -> QName -> Type -> TCM ()
addTypedInstance KwRange
r 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 IsRecord_ conName uc [] contype s

      -- Check that the sort admits record declarations.
      checkDataSort name s

      -- Make a note of what variable is the 'self' variable in the telescope.
      let info = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
RecordSelf 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 t. a -> Dom' t a
defaultDom Type
rect)

      let 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)
      modifyContextInfo hideExplicit $ 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 hideExplicit $ do
        params  <- 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 <- fromMaybe __IMPOSSIBLE__ . cxLookup 0 <$> getContext
            return $ contextToTel $ CxExtend r params
          cp <- viewTC eCurrentCheckpoint
          setModuleCheckpoint m cp
          checkRecordProjections m name hasNamedCon con tel' ftel fields


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

  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


{-| @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
-> [Declaration]
-> TCM ()
checkRecordProjections ModuleName
m QName
r Bool
hasNamedCon ConHead
con Telescope
tel Telescope
ftel [Declaration]
fs = do
    Telescope -> Telescope -> [Term] -> [Declaration] -> TCM ()
checkProjs Telescope
forall a. Tele a
EmptyTel Telescope
ftel [] [Declaration]
fs
  where

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

    checkProjs :: Telescope -> Telescope -> [Term] -> [Declaration] -> 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 List1 Declaration
fs' : [Declaration]
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] -> [Declaration] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (List1 Declaration -> [Item (List1 Declaration)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Declaration
fs' [Declaration] -> [Declaration] -> [Declaration]
forall a. [a] -> [a] -> [a]
++! [Declaration]
fs)

    -- Case: projection.
    checkProjs Telescope
ftel1 (ExtendTel (dom :: Dom Type
dom@(Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
t)) Abs Telescope
ftel2) [Term]
vs (A.Field DefInfo
info QName
x Arg Expr
_ : [Declaration]
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
      let ai :: ArgInfo
ai = Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
      -- 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 -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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...
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj.escapeContext" Nat
45 (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)
          ]
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
<+> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Nat -> tcm a -> tcm a
unsafeEscapeContext 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
<+> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Nat -> tcm a -> tcm a
unsafeEscapeContext 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
<+> Nat -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Nat -> tcm a -> tcm a
unsafeEscapeContext 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)
          ]
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
          ]
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
<+> (VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc)
-> (IsAbstract -> VerboseKey) -> IsAbstract -> TCMT IO 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)
          ]

      -- The telescope tel includes the variable of record type as last one
      -- e.g. for cartesion product it is
      --
      --   tel = {A' : Type} {B' : Type} (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' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term]
vs) Type
t'
          finalt :: Type
finalt   = Telescope -> Type -> Type
telePi 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]
          -- the recursive call
          recurse :: TCM ()
recurse  = Telescope -> Telescope -> [Term] -> [Declaration] -> 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
$ ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName (Name -> ArgName) -> Name -> ArgName
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) [Declaration]
fs

      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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

      do
        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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

        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 (ArgName, Type)]
telList = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
            ([Dom' Term (ArgName, Type)]
ptelList,[Dom' Term (ArgName, Type)
rt]) = Nat
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, 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' Term (ArgName, Type)]
telList
            ptel :: Telescope
ptel   = [Dom' Term (ArgName, Type)] -> Telescope
telFromList [Dom' Term (ArgName, 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
$ ((ArgName, Type) -> Type) -> Dom' Term (ArgName, 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 (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd Dom' Term (ArgName, 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
$ 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 :: Catchall
clauseCatchall  = Catchall
forall a. Null a => a
empty
                            , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive
                            , 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 a. a -> Arg a
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 ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type) -> Arg ArgName)
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term ArgName -> Arg ArgName)
-> (Dom' Term (ArgName, Type) -> Dom' Term ArgName)
-> Dom' Term (ArgName, Type)
-> Arg ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst) [Dom' Term (ArgName, Type)]
telList
              }

        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
          ]
        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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 (Telescope, QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (Telescope, 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
          let fun = FunctionData
emptyFunctionData
          addConstant projname $
            (defaultDefn ai projname (killRange finalt) $ 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
kwr -> KwRange -> QName -> Type -> TCM ()
addTypedInstance KwRange
kwr 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 (Declaration
d : [Declaration]
fs) = do
      Declaration -> TCM ()
checkDecl Declaration
d
      Telescope -> Telescope -> [Term] -> [Declaration] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs [Declaration]
fs