{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Monad.Signature where

import Prelude hiding (null)

import qualified Control.Monad.Fail as Fail

import Control.Arrow                 ( first, second )
import Control.Monad.Except          ( ExceptT )
import Control.Monad.State           ( StateT  )
import Control.Monad.Reader          ( ReaderT )
import Control.Monad.Writer          ( WriterT )
import Control.Monad.Trans.Maybe     ( MaybeT  )
import Control.Monad.Trans.Identity  ( IdentityT )
import Control.Monad.Trans           ( MonadTrans, lift )

import Data.Foldable (for_)
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as HMap
import Data.Maybe
import Data.Semigroup ((<>))

import Agda.Interaction.Options

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract (Ren, ScopeCopyInfo(..))
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Names
import Agda.Syntax.Position
import Agda.Syntax.Treeless (Compiled(..), TTerm, ArgUsage)

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Mutual
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import {-# SOURCE #-} Agda.TypeChecking.InstanceArguments
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
import {-# SOURCE #-} Agda.TypeChecking.Polarity
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike
import {-# SOURCE #-} Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Opacity

import {-# SOURCE #-} Agda.Compiler.Treeless.Erase
import {-# SOURCE #-} Agda.Compiler.Builtin

import Agda.Utils.CallStack.Base
import Agda.Utils.Either
import Agda.Utils.Function ( applyWhen )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (Doc, prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Update

import Agda.Utils.Impossible

-- | If the first argument is @'Erased' something@, then hard
-- compile-time mode is enabled when the continuation is run.

setHardCompileTimeModeIfErased
  :: Erased
  -> TCM a
     -- ^ Continuation.
  -> TCM a
setHardCompileTimeModeIfErased :: forall a. Erased -> TCM a -> TCM a
setHardCompileTimeModeIfErased Erased
erased =
  (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
    ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ Bool -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Erased -> Bool
isErased Erased
erased) (Lens' TCEnv Bool -> LensSet TCEnv Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardCompileTimeMode Bool
True)
    (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv Quantity -> LensMap TCEnv Quantity
forall o i. Lens' o i -> LensMap o i
over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity (Quantity -> Quantity -> Quantity
`composeQuantity` Erased -> Quantity
asQuantity Erased
erased)

-- | If the quantity is \"erased\", then hard compile-time mode is
-- enabled when the continuation is run.
--
-- Precondition: The quantity must not be @'Quantity1' something@.

setHardCompileTimeModeIfErased'
  :: LensQuantity q
  => q
     -- ^ The quantity.
  -> TCM a
     -- ^ Continuation.
  -> TCM a
setHardCompileTimeModeIfErased' :: forall q a. LensQuantity q => q -> TCM a -> TCM a
setHardCompileTimeModeIfErased' =
  Erased -> TCM a -> TCM a
forall a. Erased -> TCM a -> TCM a
setHardCompileTimeModeIfErased (Erased -> TCM a -> TCM a) -> (q -> Erased) -> q -> TCM a -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Erased -> Maybe Erased -> Erased
forall a. a -> Maybe a -> a
fromMaybe Erased
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Erased -> Erased) -> (q -> Maybe Erased) -> q -> Erased
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Maybe Erased
erasedFromQuantity (Quantity -> Maybe Erased) -> (q -> Quantity) -> q -> Maybe Erased
forall b c a. (b -> c) -> (a -> b) -> a -> c
. q -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity

-- | Use run-time mode in the continuation unless the current mode is
-- the hard compile-time mode.

setRunTimeModeUnlessInHardCompileTimeMode
  :: TCM a
     -- ^ Continuation.
  -> TCM a
setRunTimeModeUnlessInHardCompileTimeMode :: forall a. TCM a -> TCM a
setRunTimeModeUnlessInHardCompileTimeMode TCM a
c =
  TCMT IO Bool -> TCM a -> TCM a -> TCM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardCompileTimeMode) TCM a
c (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
  (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' TCEnv Quantity -> LensMap TCEnv Quantity
forall o i. Lens' o i -> LensMap o i
over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity LensMap TCEnv Quantity -> LensMap TCEnv Quantity
forall a b. (a -> b) -> a -> b
$ (Quantity -> Quantity) -> Quantity -> Quantity
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
`addQuantity` Quantity
topQuantity)) TCM a
c

-- | Use hard compile-time mode in the continuation if the first
-- argument is @'Erased' something@. Use run-time mode if the first
-- argument is @'NotErased' something@ and the current mode is not
-- hard compile-time mode.

setModeUnlessInHardCompileTimeMode
  :: Erased
  -> TCM a
     -- ^ Continuation.
  -> TCM a
setModeUnlessInHardCompileTimeMode :: forall a. Erased -> TCM a -> TCM a
setModeUnlessInHardCompileTimeMode Erased
erased TCM a
c = case Erased
erased of
  Erased{}    -> Erased -> TCM a -> TCM a
forall a. Erased -> TCM a -> TCM a
setHardCompileTimeModeIfErased Erased
erased TCM a
c
  NotErased{} -> do
    Erased -> TCM ()
warnForPlentyInHardCompileTimeMode Erased
erased
    TCM a -> TCM a
forall a. TCM a -> TCM a
setRunTimeModeUnlessInHardCompileTimeMode TCM a
c

-- | Warn if the user explicitly wrote @@ω@ or @@plenty@ but the
-- current mode is the hard compile-time mode.

warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()
warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()
warnForPlentyInHardCompileTimeMode = \case
  Erased{}    -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  NotErased QωOrigin
o -> do
    let warn :: TCM ()
warn = Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QωOrigin -> Warning
PlentyInHardCompileTimeMode QωOrigin
o
    hard <- Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardCompileTimeMode
    if not hard then return () else case o of
      QωInferred{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Qω{}         -> TCM ()
warn
      QωPlenty{}   -> TCM ()
warn

-- | Add a constant to the signature. Lifts the definition to top level.
addConstant :: QName -> Definition -> TCM ()
addConstant :: QName -> Definition -> TCM ()
addConstant QName
q Definition
d = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.signature" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding constant " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" to signature"

  -- Every constant that gets added to the signature in hard
  -- compile-time mode is treated as erased.
  hard <- Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardCompileTimeMode
  d    <- if not hard then return d else do
    case erasedFromQuantity (getQuantity d) of
      Maybe Erased
Nothing     -> TCMT IO Definition
forall a. HasCallStack => a
__IMPOSSIBLE__
      Just Erased
erased -> do
        Erased -> TCM ()
warnForPlentyInHardCompileTimeMode Erased
erased
        Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ (Quantity -> Quantity) -> Definition -> Definition
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity
zeroQuantity Quantity -> Quantity -> Quantity
`composeQuantity`) Definition
d

  tel <- getContextTelescope
  let tel' = [Char] -> Telescope -> Telescope
forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
"r" (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope
forall a. KillRange a => KillRangeT a
killRange (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
d of
              Constructor{} -> (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
hideOrKeepInstance Telescope
tel
              Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projIndex :: Projection -> Int
projIndex = Int
n } } ->
                let fallback :: Telescope
fallback = (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
hideOrKeepInstance Telescope
tel in
                if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Telescope
fallback else
                -- if the record value is part of the telescope, its hiding should left unchanged
                  case [Dom ([Char], Type)]
-> Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
forall a. [a] -> Maybe ([a], a)
initLast ([Dom ([Char], Type)]
 -> Maybe ([Dom ([Char], Type)], Dom ([Char], Type)))
-> [Dom ([Char], Type)]
-> Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel of
                    Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
Nothing -> Telescope
fallback
                    Just ([Dom ([Char], Type)]
doms, Dom ([Char], Type)
dom) -> [Dom ([Char], Type)] -> Telescope
telFromList ([Dom ([Char], Type)] -> Telescope)
-> [Dom ([Char], Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> Dom ([Char], Type))
-> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom ([Char], Type) -> Dom ([Char], Type)
forall a. LensHiding a => a -> a
hideOrKeepInstance [Dom ([Char], Type)]
doms [Dom ([Char], Type)]
-> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. [a] -> [a] -> [a]
++ [Dom ([Char], Type)
dom]
              Defn
_ -> Telescope
tel
  let d' = Telescope -> Definition -> Definition
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel' (Definition -> Definition) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Definition
d { defName = q }
  reportSDoc "tc.signature" 60 $ "lambda-lifted definition =" <?> pretty d'
  modifySignature $ updateDefinitions $ HMap.insertWith (+++) q d'
  i <- currentOrFreshMutualBlock
  setMutualBlock i q
  where
    Definition
new +++ :: Definition -> Definition -> Definition
+++ Definition
old = Definition
new { defDisplay = defDisplay new ++ defDisplay old
                      , defInstance = defInstance new `mplus` defInstance old }

-- | A combination of 'addConstant' and 'defaultDefn'. The 'Language'
-- does not need to be supplied.

addConstant' ::
  QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' :: QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
info QName
x Type
t Defn
def = do
  lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
  addConstant q $ defaultDefn info x t lang def

-- | Set termination info of a defined function symbol.
setTerminates :: MonadTCState m => QName -> Bool -> m ()
setTerminates :: forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
b = (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    def :: Defn
def@Function{} -> Defn
def { funTerminates = Just b }
    def :: Defn
def@Record{}   -> Defn
def { recTerminates = Just b }
    Defn
def -> Defn
def

-- | Set CompiledClauses of a defined function symbol.
setCompiledClauses :: QName -> CompiledClauses -> TCM ()
setCompiledClauses :: QName -> CompiledClauses -> TCM ()
setCompiledClauses QName
q CompiledClauses
cc = (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Defn -> Defn
setT
  where
    setT :: Defn -> Defn
setT def :: Defn
def@Function{} = Defn
def { funCompiled = Just cc }
    setT Defn
def            = Defn
def

-- | Set SplitTree of a defined function symbol.
setSplitTree :: QName -> SplitTree -> TCM ()
setSplitTree :: QName -> SplitTree -> TCM ()
setSplitTree QName
q SplitTree
st = (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Defn -> Defn
setT
  where
    setT :: Defn -> Defn
setT def :: Defn
def@Function{} = Defn
def { funSplitTree = Just st }
    setT Defn
def            = Defn
def

-- | Modify the clauses of a function.
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
modifyFunClauses QName
q [Clause] -> [Clause]
f =
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ ([Clause] -> [Clause]) -> Defn -> Defn
updateFunClauses [Clause] -> [Clause]
f

-- | Lifts clauses to the top-level and adds them to definition.
--   Also adjusts the 'funCopatternLHS' field if necessary.
addClauses :: (MonadConstraint m, MonadTCState m) => QName -> [Clause] -> m ()
addClauses :: forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
q [Clause]
cls = do
  tel <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  modifySignature $ updateDefinition q $
    updateTheDef (updateFunClauses (++ abstract tel cls))
    . updateDefCopatternLHS (|| isCopatternLHS cls)

  -- Jesper, 2022-10-13: unblock any constraints that were
  -- waiting for more clauses of this function
  wakeConstraints' $ wakeIfBlockedOnDef q . constraintUnblocker

mkPragma :: String -> TCM CompilerPragma
mkPragma :: [Char] -> TCM CompilerPragma
mkPragma [Char]
s = Range -> [Char] -> CompilerPragma
CompilerPragma (Range -> [Char] -> CompilerPragma)
-> TCMT IO Range -> TCMT IO ([Char] -> CompilerPragma)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange TCMT IO ([Char] -> CompilerPragma)
-> TCMT IO [Char] -> TCM CompilerPragma
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Char] -> TCMT IO [Char]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
s

-- | Add a compiler pragma `{-\# COMPILE <backend> <name> <text> \#-}`
addPragma :: BackendName -> QName -> String -> TCM ()
addPragma :: [Char] -> QName -> [Char] -> TCM ()
addPragma [Char]
b QName
q [Char]
s = TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
erased
  {- then -} (Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> QName -> Warning
PragmaCompileErased [Char]
b QName
q)
  {- else -} (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    pragma <- [Char] -> TCM CompilerPragma
mkPragma [Char]
s
    modifySignature $ updateDefinition q $ addCompilerPragma b pragma

  where

  erased :: TCM Bool
  erased :: TCMT IO Bool
erased = do
    def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
    case def of
      -- If we have a defined symbol, we check whether it is erasable
      Function{} ->
        Lens' TCEnv (Maybe [Char])
-> (Maybe [Char] -> Maybe [Char]) -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC      (Maybe [Char] -> f (Maybe [Char])) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe [Char])
eActiveBackendName (Maybe [Char] -> Maybe [Char] -> Maybe [Char]
forall a b. a -> b -> a
const (Maybe [Char] -> Maybe [Char] -> Maybe [Char])
-> Maybe [Char] -> Maybe [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
b) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$
        Lens' TCState [Backend]
-> ([Backend] -> [Backend]) -> TCMT IO Bool -> TCMT IO Bool
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState ([Backend] -> f [Backend]) -> TCState -> f TCState
Lens' TCState [Backend]
stBackends         ([Backend] -> [Backend] -> [Backend]
forall a b. a -> b -> a
const ([Backend] -> [Backend] -> [Backend])
-> [Backend] -> [Backend] -> [Backend]
forall a b. (a -> b) -> a -> b
$ [Backend]
builtinBackends) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$
        QName -> TCMT IO Bool
isErasable QName
q
     -- Otherwise (Axiom, Datatype, Record type, etc.) we keep it
      Defn
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma :: [Char] -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma [Char]
backend QName
q = do
  ps <- [Char] -> Definition -> [CompilerPragma]
defCompilerPragmas [Char]
backend (Definition -> [CompilerPragma])
-> TCMT IO Definition -> TCMT IO [CompilerPragma]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case ps of
    []  -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CompilerPragma
forall a. Maybe a
Nothing
    [CompilerPragma
p] -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CompilerPragma -> TCM (Maybe CompilerPragma))
-> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
forall a b. (a -> b) -> a -> b
$ CompilerPragma -> Maybe CompilerPragma
forall a. a -> Maybe a
Just CompilerPragma
p
    (CompilerPragma
_:CompilerPragma
p1:[CompilerPragma]
_) ->
      CompilerPragma
-> TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange CompilerPragma
p1 (TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma))
-> TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma)
forall a b. (a -> b) -> a -> b
$
            Doc -> TCM (Maybe CompilerPragma)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM (Maybe CompilerPragma))
-> TCMT IO Doc -> TCM (Maybe CompilerPragma)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Conflicting " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
backend [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" pragmas for") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"at") Int
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
"-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (CompilerPragma -> Range
forall a. HasRange a => a -> Range
getRange CompilerPragma
p) | CompilerPragma
p <- [CompilerPragma]
ps ]

setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag FunctionFlag
flag Bool
val QName
q = QName -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> TCM ())
-> (Definition -> Definition) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Lens' Definition Bool -> LensSet Definition Bool
forall o i. Lens' o i -> LensSet o i
set ((Defn -> f Defn) -> Definition -> f Definition
Lens' Definition Defn
lensTheDef ((Defn -> f Defn) -> Definition -> f Definition)
-> ((Bool -> f Bool) -> Defn -> f Defn)
-> (Bool -> f Bool)
-> Definition
-> f Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionFlag -> Lens' Defn Bool
funFlag FunctionFlag
flag) Bool
val

markStatic :: QName -> TCM ()
markStatic :: QName -> TCM ()
markStatic = FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag FunctionFlag
FunStatic Bool
True

markInline :: Bool -> QName -> TCM ()
markInline :: Bool -> QName -> TCM ()
markInline Bool
b = FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag FunctionFlag
FunInline Bool
b

markInjective :: QName -> TCM ()
markInjective :: QName -> TCM ()
markInjective QName
q = QName -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> TCM ())
-> (Definition -> Definition) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Definition
def -> Definition
def { defInjective = True }

markFirstOrder :: QName -> TCM ()
markFirstOrder :: QName -> TCM ()
markFirstOrder = FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag FunctionFlag
FunFirstOrder Bool
True

unionSignatures :: [Signature] -> Signature
unionSignatures :: [Signature] -> Signature
unionSignatures [Signature]
ss = (Signature -> Signature -> Signature)
-> Signature -> [Signature] -> Signature
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Signature -> Signature -> Signature
unionSignature Signature
emptySignature [Signature]
ss
  where
    unionSignature :: Signature -> Signature -> Signature
unionSignature (Sig Sections
a Definitions
b RewriteRuleMap
c InstanceTable
d) (Sig Sections
a' Definitions
b' RewriteRuleMap
c' InstanceTable
d') =
      Sections
-> Definitions -> RewriteRuleMap -> InstanceTable -> Signature
Sig (Sections -> Sections -> Sections
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Sections
a Sections
a')
          (Definitions -> Definitions -> Definitions
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HMap.union Definitions
b Definitions
b')             -- definitions are unique (in at most one module)
          ((RewriteRules -> RewriteRules -> RewriteRules)
-> RewriteRuleMap -> RewriteRuleMap -> RewriteRuleMap
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith RewriteRules -> RewriteRules -> RewriteRules
forall a. Monoid a => a -> a -> a
mappend RewriteRuleMap
c RewriteRuleMap
c') -- rewrite rules are accumulated
          (InstanceTable
d InstanceTable -> InstanceTable -> InstanceTable
forall a. Semigroup a => a -> a -> a
<> InstanceTable
d')                     -- instances are accumulated

-- | Add a section to the signature.
--
--   The current context will be stored as the cumulative module parameters
--   for this section.
addSection :: ModuleName -> TCM ()
addSection :: ModuleName -> TCM ()
addSection ModuleName
m = do
  tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let sec = Telescope -> Section
Section Telescope
tel
  -- Make sure we do not overwrite an existing section!
  whenJustM (getSection m) $ \ Section
sec' -> do
    -- At least not with different content!
    if (Section
sec Section -> Section -> Bool
forall a. Eq a => a -> a -> Bool
== Section
sec') then do
      -- Andreas, 2015-12-02: test/Succeed/Issue1701II.agda
      -- reports a "redundantly adding existing section".
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"warning: redundantly adding existing section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with content" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
    else do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"overwriting existing section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"of content  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec'
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with content" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
      TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  -- Add the new section.
  setModuleCheckpoint m
  modifySignature $ over sigSections $ Map.insert m sec

-- | Sets the checkpoint for the given module to the current checkpoint.
setModuleCheckpoint :: ModuleName -> TCM ()
setModuleCheckpoint :: ModuleName -> TCM ()
setModuleCheckpoint ModuleName
m = do
  chkpt <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  stModuleCheckpoints `modifyTCLens` Map.insert m chkpt

-- | Get a section.
--
--   Why Maybe? The reason is that we look up all prefixes of a module to
--   compute number of parameters, and for hierarchical top-level modules,
--   A.B.C say, A and A.B do not exist.
{-# SPECIALIZE getSection :: ModuleName -> TCM (Maybe Section) #-}
{-# SPECIALIZE getSection :: ModuleName -> ReduceM (Maybe Section) #-}
getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
getSection :: forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m = do
  sig  <- (TCState -> Lens' TCState Sections -> Sections
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Sections -> f Sections) -> Signature -> f Signature)
-> (Sections -> f Sections)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sections -> f Sections) -> Signature -> f Signature
Lens' Signature Sections
sigSections) (TCState -> Sections) -> m TCState -> m Sections
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  isig <- (^. stImports   . sigSections) <$> getTCState
  return $ Map.lookup m sig `mplus` Map.lookup m isig

-- | Lookup a section telescope.
--
--   If it doesn't exist, like in hierarchical top-level modules,
--   the section telescope is empty.
{-# SPECIALIZE lookupSection :: ModuleName -> TCM Telescope #-}
{-# SPECIALIZE lookupSection :: ModuleName -> ReduceM Telescope #-}
lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
lookupSection :: forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m = Telescope -> (Section -> Telescope) -> Maybe Section -> Telescope
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Telescope
forall a. Tele a
EmptyTel (Section -> Lens' Section Telescope -> Telescope
forall o i. o -> Lens' o i -> i
^. (Telescope -> f Telescope) -> Section -> f Section
Lens' Section Telescope
secTelescope) (Maybe Section -> Telescope) -> m (Maybe Section) -> m Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Maybe Section)
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m

-- | Add display forms for a name @f@ copied by a module application. Essentially if @f@ can reduce to
--
-- @
-- λ xs → A.B.C.f vs
-- @
--
-- by unfolding module application copies (`defCopy`), then we add a display form
--
-- @
-- A.B.C.f vs ==> f xs
-- @
addDisplayForms :: QName -> TCM ()
addDisplayForms :: QName -> TCM ()
addDisplayForms QName
x = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.display.section" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Computing display forms for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x
  def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  let v = case Definition -> Defn
theDef Definition
def of
             Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
h} -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
h{ conName = x } ConInfo
ConOSystem []
             Defn
_                          -> QName -> Elims -> Term
Def QName
x []

  -- Compute all unfoldings of x by repeatedly calling reduceDefCopy
  vs <- unfoldings x v
  reportSDoc "tc.display.section" 20 $ nest 2 $ vcat
    [ "unfoldings:" <?> vcat [ "-" <+> pretty v | v <- vs ] ]

  -- Turn unfoldings into display forms
  npars <- subtract (projectionArgs def) <$> getContextSize
  let dfs = (Term -> (QName, DisplayForm)) -> [Term] -> [(QName, DisplayForm)]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Term -> Term -> (QName, DisplayForm)
displayForm Int
npars Term
v) [Term]
vs
  reportSDoc "tc.display.section" 20 $ nest 2 $ vcat
    [ "displayForms:" <?> vcat [ "-" <+> (pretty y <+> "-->" <?> pretty df) | (y, df) <- dfs ] ]

  -- and add them
  mapM_ (uncurry addDisplayForm) dfs
  where

    -- To get display forms for projections we need to unSpine here.
    view :: Term -> ([Arg ArgName], Term)
    view :: Term -> ([Arg [Char]], Term)
view = (Term -> Term) -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Term -> Term
unSpine (([Arg [Char]], Term) -> ([Arg [Char]], Term))
-> (Term -> ([Arg [Char]], Term)) -> Term -> ([Arg [Char]], Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ([Arg [Char]], Term)
lamView

    -- Given an unfolding `top = λ xs → y es` generate a display form
    -- `y es ==> top xs`. The first `npars` variables in `xs` are module parameters
    -- and should not be pattern variables, but matched literally.
    displayForm :: Nat -> Term -> Term -> (QName, DisplayForm)
    displayForm :: Int -> Term -> Term -> (QName, DisplayForm)
displayForm Int
npars Term
top Term
v =
      case Term -> ([Arg [Char]], Term)
view Term
v of
        ([Arg [Char]]
xs, Def QName
y Elims
es)   -> (QName
y,)         (DisplayForm -> (QName, DisplayForm))
-> DisplayForm -> (QName, DisplayForm)
forall a b. (a -> b) -> a -> b
$ [Arg [Char]] -> Elims -> DisplayForm
mkDisplay [Arg [Char]]
xs Elims
es
        ([Arg [Char]]
xs, Con ConHead
h ConInfo
i Elims
es) -> (ConHead -> QName
conName ConHead
h,) (DisplayForm -> (QName, DisplayForm))
-> DisplayForm -> (QName, DisplayForm)
forall a b. (a -> b) -> a -> b
$ [Arg [Char]] -> Elims -> DisplayForm
mkDisplay [Arg [Char]]
xs Elims
es
        ([Arg [Char]], Term)
_ -> (QName, DisplayForm)
forall a. HasCallStack => a
__IMPOSSIBLE__
      where
        mkDisplay :: [Arg [Char]] -> Elims -> DisplayForm
mkDisplay [Arg [Char]]
xs Elims
es = Int -> Elims -> DisplayTerm -> DisplayForm
Display (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
npars) Elims
es (DisplayTerm -> DisplayForm) -> DisplayTerm -> DisplayForm
forall a b. (a -> b) -> a -> b
$ Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term
top Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args
          -- Andreas, 2023-01-26, #6476:
          -- I think this @apply@ is safe (rather than @DTerm' top (map Apply args)@).
          where
            n :: Int
n    = [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs
            args :: [Arg Term]
args = (Arg [Char] -> Int -> Arg Term)
-> [Arg [Char]] -> [Int] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg [Char]
x Int
i -> Int -> Term
var Int
i Term -> Arg [Char] -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char]
x) [Arg [Char]]
xs (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n)

    -- Unfold a single defCopy.
    unfoldOnce :: Term -> TCM (Reduced () Term)
    unfoldOnce :: Term -> TCM (Reduced () Term)
unfoldOnce Term
v = case Term -> ([Arg [Char]], Term)
view Term
v of
      ([Arg [Char]]
xs, Def QName
f Elims
es)   -> ((Reduced () Term -> Reduced () Term)
-> TCM (Reduced () Term) -> TCM (Reduced () Term)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Reduced () Term -> Reduced () Term)
 -> TCM (Reduced () Term) -> TCM (Reduced () Term))
-> ((Term -> Term) -> Reduced () Term -> Reduced () Term)
-> (Term -> Term)
-> TCM (Reduced () Term)
-> TCM (Reduced () Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term) -> Reduced () Term -> Reduced () Term
forall a b. (a -> b) -> Reduced () a -> Reduced () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM QName
f Elims
es)
      ([Arg [Char]]
xs, Con ConHead
c ConInfo
i Elims
es) -> ((Reduced () Term -> Reduced () Term)
-> TCM (Reduced () Term) -> TCM (Reduced () Term)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Reduced () Term -> Reduced () Term)
 -> TCM (Reduced () Term) -> TCM (Reduced () Term))
-> ((Term -> Term) -> Reduced () Term -> Reduced () Term)
-> (Term -> Term)
-> TCM (Reduced () Term)
-> TCM (Reduced () Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term) -> Reduced () Term -> Reduced () Term
forall a b. (a -> b) -> Reduced () a -> Reduced () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM (ConHead -> QName
conName ConHead
c) Elims
es)
      ([Arg [Char]], Term)
_                -> Reduced () Term -> TCM (Reduced () Term)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduced () Term -> TCM (Reduced () Term))
-> Reduced () Term -> TCM (Reduced () Term)
forall a b. (a -> b) -> a -> b
$ () -> Reduced () Term
forall no yes. no -> Reduced no yes
NoReduction ()

    -- Compute all reduceDefCopy unfoldings of `x`. Stop when we hit a non-copy.
    unfoldings :: QName -> Term -> TCM [Term]
    unfoldings :: QName -> Term -> TCM [Term]
unfoldings QName
x Term
v = Term -> TCM (Reduced () Term)
unfoldOnce Term
v TCM (Reduced () Term)
-> (Reduced () Term -> TCM [Term]) -> TCM [Term]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      NoReduction{}     -> [Term] -> TCM [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      YesReduction Simplification
_ Term
v' -> do
        let headSymbol :: Maybe QName
headSymbol = case ([Arg [Char]], Term) -> Term
forall a b. (a, b) -> b
snd (([Arg [Char]], Term) -> Term) -> ([Arg [Char]], Term) -> Term
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
view Term
v' of
              Def QName
y Elims
_   -> QName -> Maybe QName
forall a. a -> Maybe a
Just QName
y
              Con ConHead
y ConInfo
_ Elims
_ -> QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
y)
              Term
_         -> Maybe QName
forall a. Maybe a
Nothing
        case Maybe QName
headSymbol of
          Maybe QName
Nothing -> [Term] -> TCM [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          Just QName
y | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y -> do
            -- This should never happen, but if it does, getting an __IMPOSSIBLE__ is much better
            -- than looping.
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
"reduceDefCopy said YesReduction but the head symbol is the same!?"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v'
              ]
            TCM [Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
          Just QName
y -> do
            TCMT IO Bool -> TCM [Term] -> TCM [Term] -> TCM [Term]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Definition -> Bool
defCopy (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
y)
                ((Term
v' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) ([Term] -> [Term]) -> TCM [Term] -> TCM [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Term -> TCM [Term]
unfoldings QName
y Term
v')  -- another copy so keep going
                ([Term] -> TCM [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Term
v'])                 -- not a copy, we stop

-- | Module application (followed by module parameter abstraction).
applySection
  :: ModuleName     -- ^ Name of new module defined by the module macro.
  -> Telescope      -- ^ Parameters of new module.
  -> ModuleName     -- ^ Name of old module applied to arguments.
  -> Args           -- ^ Arguments of module application.
  -> ScopeCopyInfo  -- ^ Imported names and modules
  -> TCM ()
applySection :: ModuleName
-> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
applySection ModuleName
new Telescope
ptel ModuleName
old [Arg Term]
ts ScopeCopyInfo{ renModules :: ScopeCopyInfo -> Ren ModuleName
renModules = Ren ModuleName
rm, renNames :: ScopeCopyInfo -> Ren QName
renNames = Ren QName
rd } = do
  rd <- Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
rd
  applySection' new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = rd }
  where
    -- If a datatype is being copied, all its constructors need to be copied,
    -- and if a constructor is copied its datatype needs to be.
    closeConstructors :: Ren QName -> TCM (Ren QName)
    closeConstructors :: Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
rd = do
        ds <- ((ModuleName, QName) -> QName)
-> [(ModuleName, QName)] -> [(ModuleName, QName)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (ModuleName, QName) -> QName
forall a b. (a, b) -> b
snd ([(ModuleName, QName)] -> [(ModuleName, QName)])
-> ([Maybe (ModuleName, QName)] -> [(ModuleName, QName)])
-> [Maybe (ModuleName, QName)]
-> [(ModuleName, QName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (ModuleName, QName)] -> [(ModuleName, QName)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (ModuleName, QName)] -> [(ModuleName, QName)])
-> TCMT IO [Maybe (ModuleName, QName)]
-> TCMT IO [(ModuleName, QName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName)))
-> [(QName, List1 QName)] -> TCMT IO [Maybe (ModuleName, QName)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName))
constructorData (Ren QName -> [(QName, List1 QName)]
forall k a. Map k a -> [(k, a)]
Map.toList Ren QName
rd)
        cs <- nubOn snd . concat    <$> traverse dataConstructors (Map.toList rd)
        new <- Map.unionsWith (<>) <$> traverse rename (ds ++ cs)
        reportSDoc "tc.mod.apply.complete" 30 $
          "also copying: " <+> pretty new
        return $ Map.unionWith (<>) new rd
      where
        rename :: (ModuleName, QName) -> TCM (Ren QName)
        rename :: (ModuleName, QName) -> TCM (Ren QName)
rename (ModuleName
m, QName
x)
          | QName
x QName -> Ren QName -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Ren QName
rd = Ren QName -> TCM (Ren QName)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ren QName
forall a. Monoid a => a
mempty
          | Bool
otherwise =
              -- Ulf, 2024-06-24 (#7329):
              --   Here we used to generate an unqualified name, but this breaks things if the new
              --   module shows up in a module application later on. This is because we use the
              --   module name to figure out which arguments from the application are relevant for
              --   the current symbol (see argsToUse in applySection' below).
              --
              --   Instead we use the target module name of the thing that required x to be copied.
              --   For instance, if we are copying a data type A.B.D to X.Y.Z.D and its constructor
              --   mkD is not in the renaming, we add `A.B.mkD -> X.Y.Z.mkD` (instead of `A.B.mkD ->
              --   mkD` which we did before).
              QName -> List1 QName -> Ren QName
forall k a. k -> a -> Map k a
Map.singleton QName
x (List1 QName -> Ren QName)
-> (Name -> List1 QName) -> Name -> Ren QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 QName
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> List1 QName) -> (Name -> QName) -> Name -> List1 QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
qualify ModuleName
m (Name -> Ren QName) -> TCMT IO Name -> TCM (Ren QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => [Char] -> m Name
freshName_ (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)

        constructorData :: (QName, List1.List1 QName) -> TCM (Maybe (ModuleName, QName))
        constructorData :: (QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName))
constructorData (QName
x, QName
y List1.:| [QName]
_) = do  -- All new names share the same module, so we can safely grab the first one
          (Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x) TCMT IO Defn
-> (Defn -> Maybe (ModuleName, QName))
-> TCMT IO (Maybe (ModuleName, QName))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Constructor{ conData :: Defn -> QName
conData = QName
d } -> (ModuleName, QName) -> Maybe (ModuleName, QName)
forall a. a -> Maybe a
Just (QName -> ModuleName
qnameModule QName
y, QName
d)
            Defn
_                          -> Maybe (ModuleName, QName)
forall a. Maybe a
Nothing

        dataConstructors :: (QName, List1.List1 QName) -> TCM [(ModuleName, QName)]
        dataConstructors :: (QName, List1 QName) -> TCMT IO [(ModuleName, QName)]
dataConstructors (QName
x, QName
y List1.:| [QName]
_) = do
          (Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x) TCMT IO Defn
-> (Defn -> [(ModuleName, QName)]) -> TCMT IO [(ModuleName, QName)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> (QName -> (ModuleName, QName)) -> [QName] -> [(ModuleName, QName)]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> ModuleName
qnameModule QName
y,) [QName]
cs
            Record{ recConHead :: Defn -> ConHead
recConHead = ConHead
h }  -> [(QName -> ModuleName
qnameModule QName
y, ConHead -> QName
conName ConHead
h)]
            Defn
_                         -> []

applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection' :: ModuleName
-> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
applySection' ModuleName
new Telescope
ptel ModuleName
old [Arg Term]
ts ScopeCopyInfo{ renNames :: ScopeCopyInfo -> Ren QName
renNames = Ren QName
rd, renModules :: ScopeCopyInfo -> Ren ModuleName
renModules = Ren ModuleName
rm } = do
  do
    noCopyList <- [Maybe QName] -> [QName]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe QName] -> [QName])
-> TCMT IO [Maybe QName] -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PrimitiveId -> TCMT IO (Maybe QName))
-> [PrimitiveId] -> TCMT IO [Maybe QName]
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 PrimitiveId -> TCMT IO (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' [PrimitiveId]
constrainedPrims
    for_ (Map.keys rd) $ \ QName
q ->
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QName
q QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
noCopyList) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (QName -> TypeError
TriedToCopyConstrainedPrim QName
q)

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
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
vcat
    [ TCMT IO Doc
"applySection"
    , TCMT IO Doc
"new  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
new
    , TCMT IO Doc
"ptel =" 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
ptel
    , TCMT IO Doc
"old  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
old
    , TCMT IO Doc
"ts   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Arg Term]
ts
    ]
  _ <- (QName -> List1 QName -> TCMT IO (NonEmpty ()))
-> Ren QName -> TCMT IO (Map QName (NonEmpty ()))
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey ((QName -> TCM ()) -> List1 QName -> TCMT IO (NonEmpty ())
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse ((QName -> TCM ()) -> List1 QName -> TCMT IO (NonEmpty ()))
-> (QName -> QName -> TCM ())
-> QName
-> List1 QName
-> TCMT IO (NonEmpty ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg Term] -> QName -> QName -> TCM ()
copyDef [Arg Term]
ts) Ren QName
rd
  _ <- Map.traverseWithKey (traverse . copySec ts) rm
  computePolarity (Map.elems rd >>= List1.toList)
  where
    -- Andreas, 2013-10-29
    -- Here, if the name x is not imported, it persists as
    -- old, possibly out-of-scope name.
    -- This old name may used by the case split tactic, leading to
    -- names that cannot be printed properly.
    -- I guess it would make sense to mark non-imported names
    -- as such (out-of-scope) and let splitting fail if it would
    -- produce out-of-scope constructors.
    --
    -- Taking 'List1.head' because 'Module.Data.cons' and 'Module.cons' are
    -- equivalent valid names and either can be used.
    copyName :: QName -> QName
copyName QName
x = QName -> (List1 QName -> QName) -> Maybe (List1 QName) -> QName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe QName
x List1 QName -> QName
forall a. NonEmpty a -> a
List1.head (QName -> Ren QName -> Maybe (List1 QName)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x Ren QName
rd)

    copyConHead :: ConHead -> ConHead
copyConHead ConHead
c = ConHead
c { conName = copyName (conName c) }

    argsToUse :: ModuleName -> TCMT IO Int
argsToUse ModuleName
x = do
      let m :: ModuleName
m = ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
old ModuleName
x
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Common prefix: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> TCMT IO Telescope -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m

    copyDef :: Args -> QName -> QName -> TCM ()
    copyDef :: [Arg Term] -> QName -> QName -> TCM ()
copyDef [Arg Term]
ts QName
x QName
y = do
      def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
      np  <- argsToUse (qnameModule x)
      -- Issue #3083: We need to use the hiding from the telescope of the
      -- original module. This can be different than the hiding for the common
      -- parent in the case of record modules.
      hidings <- map getHiding . telToList <$> lookupSection (qnameModule x)
      let ts' = (Hiding -> Arg Term -> Arg Term)
-> [Hiding] -> [Arg Term] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding [Hiding]
hidings [Arg Term]
ts
      commonTel <- lookupSection (commonParentModule old $ qnameModule x)
      reportSDoc "tc.mod.apply" 80 $ vcat
        [ "copyDef" <+> pretty x <+> "->" <+> pretty y
        , "ts' = " <+> pretty ts' ]
      -- The module telescope had been divided by some μ, so the corresponding
      -- top level definition had type μ \ Γ → B, so if we have a substitution
      -- Δ → Γ we actually want to apply μ \ - to it, so the new top-level
      -- definition we get will have signature μ \ Δ → B.  This is only valid
      -- for pure modality systems though.
      let ai = Definition -> ArgInfo
defArgInfo Definition
def
          m = Modality
unitModality { modCohesion = getCohesion ai }
      localTC (over eContext (map (mapModality (m `inverseComposeModality`)))) $
        copyDef' ts' np def
      where
        copyDef' :: [Arg Term] -> Int -> Definition -> TCM ()
copyDef' [Arg Term]
ts Int
np Definition
d = do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"making new def for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with" 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 (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
np) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"args" 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 (IsAbstract -> [Char]
forall a. Show a => a -> [Char]
show (IsAbstract -> [Char]) -> IsAbstract -> [Char]
forall a b. (a -> b) -> a -> b
$ Definition -> IsAbstract
defAbstract Definition
d)
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 (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
vcat
            [ TCMT IO Doc
"args = " 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 ([Arg Term] -> [Char]
forall a. Show a => a -> [Char]
show [Arg Term]
ts')
            , TCMT IO Doc
"old type = " 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 (Definition -> Type
defType Definition
d) ]
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"new type = " 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
          QName -> Definition -> TCM ()
addConstant QName
y (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
nd QName
y
          QName -> TCM ()
makeProjection QName
y
          -- Issue1238: the copied def should be an 'instance' if the original
          -- def is one. Skip constructors since the original constructor will
          -- still work as an instance.
          -- Issue5583: Don't skip constructures, because the original constructor doesn't always
          -- work. For instance if it's only available in an anonymous module generated by
          -- `open import M args`.
          Maybe InstanceInfo -> (InstanceInfo -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe InstanceInfo
inst ((InstanceInfo -> TCM ()) -> TCM ())
-> (InstanceInfo -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \InstanceInfo
_ -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCM ()
addTypedInstance' Bool
False Maybe InstanceInfo
inst QName
y Type
t
          -- Set display form for the old name if it's not a constructor.
{- BREAKS fail/Issue478
          -- Andreas, 2012-10-20 and if we are not an anonymous module
          -- unless (isAnonymousModuleName new || isCon || not (null ptel)) $ do
-}
          -- BREAKS fail/Issue1643a
          -- -- Andreas, 2015-09-09 Issue 1643:
          -- -- Do not add a display form for a bare module alias.
          -- when (not isCon && null ptel && not (null ts)) $ do
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
ptel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            QName -> TCM ()
addDisplayForms QName
y
          where
            ts' :: [Arg Term]
ts' = Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
np [Arg Term]
ts
            t :: Type
t   = Definition -> Type
defType Definition
d Type -> [Arg Term] -> Type
`piApply` [Arg Term]
ts'
            pol :: [Polarity]
pol = Definition -> [Polarity]
defPolarity Definition
d [Polarity] -> [Arg Term] -> [Polarity]
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
            occ :: [Occurrence]
occ = Definition -> [Occurrence]
defArgOccurrences Definition
d [Occurrence] -> [Arg Term] -> [Occurrence]
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
            gen :: NumGeneralizableArgs
gen = Definition -> NumGeneralizableArgs
defArgGeneralizable Definition
d NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
            inst :: Maybe InstanceInfo
inst = Definition -> Maybe InstanceInfo
defInstance Definition
d
            -- the name is set by the addConstant function
            nd :: QName -> TCM Definition
            nd :: QName -> TCMT IO Definition
nd QName
y = do
              -- The arguments may use some feature of the current
              -- language.
              lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
              for def $ \ Defn
df -> Defn
                    { defArgInfo :: ArgInfo
defArgInfo        = Definition -> ArgInfo
defArgInfo Definition
d
                    , defName :: QName
defName           = QName
y
                    , defType :: Type
defType           = Type
t
                    , defPolarity :: [Polarity]
defPolarity       = [Polarity]
pol
                    , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence]
occ
                    , defArgGeneralizable :: NumGeneralizableArgs
defArgGeneralizable = NumGeneralizableArgs
gen
                    , defGeneralizedParams :: [Maybe Name]
defGeneralizedParams = [] -- This is only needed for type checking data/record defs so no need to copy it.
                    , defDisplay :: [LocalDisplayForm]
defDisplay        = []
                    , defMutual :: MutualId
defMutual         = -MutualId
1   -- TODO: mutual block?
                    , defCompiledRep :: CompiledRepresentation
defCompiledRep    = CompiledRepresentation
noCompiledRep
                    , defInstance :: Maybe InstanceInfo
defInstance       = Maybe InstanceInfo
inst
                    , defCopy :: Bool
defCopy           = Bool
True
                    , defMatchable :: Set QName
defMatchable      = Set QName
forall a. Set a
Set.empty
                    , defNoCompilation :: Bool
defNoCompilation  = Definition -> Bool
defNoCompilation Definition
d
                    , defInjective :: Bool
defInjective      = Bool
False
                    , defCopatternLHS :: Bool
defCopatternLHS   = [Clause] -> Bool
isCopatternLHS [Clause
cl]
                    , defBlocked :: Blocked_
defBlocked        = Definition -> Blocked_
defBlocked Definition
d
                    , defLanguage :: Language
defLanguage       =
                      case Definition -> Language
defLanguage Definition
d of
                        -- Note that Cubical Agda code can be imported
                        -- when --erased-cubical is used.
                        l :: Language
l@(Cubical Cubical
CFull) -> Language
l
                        Cubical Cubical
CErased   -> Language
lang
                        Language
WithoutK          -> Language
lang
                        Language
WithK             -> Language
lang
                    , theDef :: Defn
theDef            = Defn
df }
            oldDef :: Defn
oldDef = Definition -> Defn
theDef Definition
d
            isCon :: Bool
isCon  = case Defn
oldDef of { Constructor{} -> Bool
True ; Defn
_ -> Bool
False }
            mutual :: Maybe [QName]
mutual = case Defn
oldDef of { Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
m} -> Maybe [QName]
m              ; Defn
_ -> Maybe [QName]
forall a. Maybe a
Nothing }
            extlam :: Maybe ExtLamInfo
extlam = case Defn
oldDef of { Function{funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
e} -> Maybe ExtLamInfo
e              ; Defn
_ -> Maybe ExtLamInfo
forall a. Maybe a
Nothing }
            with :: Maybe QName
with   = case Defn
oldDef of { Function{funWith :: Defn -> Maybe QName
funWith = Maybe QName
w}   -> QName -> QName
copyName (QName -> QName) -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
w ; Defn
_ -> Maybe QName
forall a. Maybe a
Nothing }
            -- Andreas, 2015-05-11, to fix issue 1413:
            -- Even if we apply the record argument (must be @var 0@), we stay a projection.
            -- This is because we may abstract the record argument later again.
            -- See succeed/ProjectionNotNormalized.agda
            isVar0 :: Arg Term -> Bool
isVar0 Arg Term
t = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t of Var Int
0 [] -> Bool
True; Term
_ -> Bool
False
            proj :: Either ProjectionLikenessMissing Projection
            proj :: Either ProjectionLikenessMissing Projection
proj   = case Defn
oldDef of
              Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right p :: Projection
p@Projection{projIndex :: Projection -> Int
projIndex = Int
n}}
                | [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
ts' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Bool -> Bool -> Bool
|| ([Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
ts' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& Bool -> (Arg Term -> Bool) -> Maybe (Arg Term) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Arg Term -> Bool
isVar0 ([Arg Term] -> Maybe (Arg Term)
forall a. [a] -> Maybe a
lastMaybe [Arg Term]
ts'))
                -> Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right Projection
p { projIndex = n - size ts'
                           , projLams  = projLams p `apply` ts'
                           , projProper= copyName <$> projProper p
                           }
              -- Preserve no-projection-likeness flag if it exists, and
              -- it's set to @Left _@. For future reference: The match
              -- on left can't be simplified or it accidentally
              -- circumvents the guard above.
              Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
projl} -> ProjectionLikenessMissing
-> Either ProjectionLikenessMissing Projection
forall a b. a -> Either a b
Left ProjectionLikenessMissing
projl
              Defn
_ -> ProjectionLikenessMissing
-> Either ProjectionLikenessMissing Projection
forall a b. a -> Either a b
Left ProjectionLikenessMissing
MaybeProjection
            def :: TCMT IO Defn
def =
              case Defn
oldDef of
                Constructor{ conPars :: Defn -> Int
conPars = Int
np, conData :: Defn -> QName
conData = QName
d } -> Defn -> TCMT IO Defn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { conPars = np - size ts'
                         , conData = copyName d
                         }
                Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> Defn -> TCMT IO Defn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { dataPars   = np - size ts'
                         , dataClause = Just cl
                         , dataCons   = map copyName cs
                         }
                Record{ recPars :: Defn -> Int
recPars = Int
np, recTel :: Defn -> Telescope
recTel = Telescope
tel, recConHead :: Defn -> ConHead
recConHead = ConHead
c, recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> Defn -> TCMT IO Defn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { recPars    = np - size ts'
                         , recClause  = Just cl
                         , recTel     = apply tel ts'
                         , recConHead = copyConHead c
                         , recFields  = (map . fmap) copyName fs
                         }
                Defn
GeneralizableVar -> Defn -> TCMT IO Defn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Defn
GeneralizableVar
                Defn
_ -> do
                  (mst, _, cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause
cl] -- Andreas, 2012-10-07 non need for record pattern translation
                  fun          <- emptyFunctionData
                  let newDef =
                        Lens' Defn Bool -> LensSet Defn Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funProj   (Defn
oldDef Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funProj) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Lens' Defn Bool -> LensSet Defn Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funMacro  (Defn
oldDef Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funMacro) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Lens' Defn Bool -> LensSet Defn Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funStatic (Defn
oldDef Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funStatic) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Lens' Defn Bool -> LensSet Defn Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funInline Bool
True (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        FunctionData -> Defn
FunctionDefn FunctionData
fun
                        { _funClauses        = [cl]
                        , _funCompiled       = Just cc
                        , _funSplitTree      = mst
                        , _funMutual         = mutual
                        , _funProjection     = proj
                        , _funTerminates     = Just True
                        , _funExtLam         = extlam
                        , _funWith           = with
                        }
                  reportSDoc "tc.mod.apply" 80 $ ("new def for" <+> pretty x) <?> pretty newDef
                  return newDef

            cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange    = [Clause] -> Range
forall a. HasRange a => a -> Range
getRange ([Clause] -> Range) -> [Clause] -> Range
forall a b. (a -> b) -> a -> b
$ Definition -> [Clause]
defClauses Definition
d
                        , clauseFullRange :: Range
clauseFullRange   = [Clause] -> Range
forall a. HasRange a => a -> Range
getRange ([Clause] -> Range) -> [Clause] -> Range
forall a b. (a -> b) -> a -> b
$ Definition -> [Clause]
defClauses Definition
d
                        , clauseTel :: Telescope
clauseTel         = Telescope
forall a. Tele a
EmptyTel
                        , namedClausePats :: NAPs
namedClausePats   = []
                        , 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
$ Int -> Term -> Term
forall a. DropArgs a => Int -> a -> a
dropArgs Int
pars (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ case Defn
oldDef of
                            Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p} -> Projection -> ProjOrigin -> Relevance -> [Arg Term] -> Term
projDropParsApply Projection
p ProjOrigin
ProjSystem Relevance
rel [Arg Term]
ts'
                            Defn
_ -> QName -> Elims -> Term
Def QName
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
ts'
                        , 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 a. a -> Arg a
defaultArg Type
t
                        , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                        , clauseExact :: Maybe Bool
clauseExact       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                        , clauseRecursive :: Maybe Bool
clauseRecursive   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -- definitely not recursive
                        , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -- definitely not unreachable
                        , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                        , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                        }
              where
                -- The number of remaining parameters. We need to drop the
                -- lambdas corresponding to these from the clause body above.
                pars :: Int
pars = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ (ProjectionLikenessMissing -> Int)
-> (Projection -> Int)
-> Either ProjectionLikenessMissing Projection
-> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> ProjectionLikenessMissing -> Int
forall a b. a -> b -> a
const Int
0) (Int -> Int
forall a. Enum a => a -> a
pred (Int -> Int) -> (Projection -> Int) -> Projection -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Projection -> Int
projIndex) Either ProjectionLikenessMissing Projection
proj
                rel :: Relevance
rel  = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (ArgInfo -> Relevance) -> ArgInfo -> Relevance
forall a b. (a -> b) -> a -> b
$ Definition -> ArgInfo
defArgInfo Definition
d

    {- Example

    module Top Θ where
      module A Γ where
        module M Φ where
      module B Δ where
        module N Ψ where
          module O Ψ' where
        open A public     -- introduces only M --> A.M into the *scope*
    module C Ξ = Top.B ts

    new section C
      tel = Ξ.(Θ.Δ)[ts]

    calls
      1. copySec ts Top.A.M C.M
      2. copySec ts Top.B.N C.N
      3. copySec ts Top.B.N.O C.N.O
    with
      old = Top.B

    For 1.
      Common prefix is: Top
      totalArgs = |Θ|   (section Top)
      tel       = Θ.Γ.Φ (section Top.A.M)
      ts'       = take totalArgs ts
      Θ₂        = drop totalArgs Θ
      new section C.M
        tel =  Θ₂.Γ.Φ[ts']
    -}
    copySec :: Args -> ModuleName -> ModuleName -> TCM ()
    copySec :: [Arg Term] -> ModuleName -> ModuleName -> TCM ()
copySec [Arg Term]
ts ModuleName
x ModuleName
y = do
      totalArgs <- ModuleName -> TCMT IO Int
argsToUse ModuleName
x
      tel       <- lookupSection x
      let sectionTel =  Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
apply Telescope
tel ([Arg Term] -> Telescope) -> [Arg Term] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
totalArgs [Arg Term]
ts
      reportSDoc "tc.mod.apply" 80 $ "Copying section" <+> pretty x <+> "to" <+> pretty y
      reportSDoc "tc.mod.apply" 80 $ "  ts           = " <+> mconcat (List.intersperse "; " (map pretty ts))
      reportSDoc "tc.mod.apply" 80 $ "  totalArgs    = " <+> text (show totalArgs)
      reportSDoc "tc.mod.apply" 80 $ "  tel          = " <+> text (unwords (map (fst . unDom) $ telToList tel))  -- only names
      reportSDoc "tc.mod.apply" 80 $ "  sectionTel   = " <+> text (unwords (map (fst . unDom) $ telToList ptel)) -- only names
      addContext sectionTel $ addSection y

-- | Add a display form to a definition (could be in this or imported signature).
addDisplayForm :: QName -> DisplayForm -> TCM ()
addDisplayForm :: QName -> DisplayForm -> TCM ()
addDisplayForm QName
x DisplayForm
df = do
  d <- DisplayForm -> TCMT IO LocalDisplayForm
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen DisplayForm
df
  let add = QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
x ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> Definition
def{ defDisplay = d : defDisplay def }
  ifM (isLocal x)
    {-then-} (modifySignature add)
    {-else-} (stImportsDisplayForms `modifyTCLens` HMap.insertWith (++) x [d])
  whenM (hasLoopingDisplayForm x) $
    typeError . GenericDocError =<< do "Cannot add recursive display form for" <+> pretty x

isLocal :: ReadTCState m => QName -> m Bool
isLocal :: forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
x = QName -> Definitions -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
HMap.member QName
x (Definitions -> Bool) -> m Definitions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState Definitions -> m Definitions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Definitions -> f Definitions) -> Signature -> f Signature)
-> (Definitions -> f Definitions)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Signature Definitions
sigDefinitions)

getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
getDisplayForms :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [LocalDisplayForm]
getDisplayForms QName
q = do
  ds  <- (SigError -> [LocalDisplayForm])
-> (Definition -> [LocalDisplayForm])
-> Either SigError Definition
-> [LocalDisplayForm]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([LocalDisplayForm] -> SigError -> [LocalDisplayForm]
forall a b. a -> b -> a
const []) Definition -> [LocalDisplayForm]
defDisplay (Either SigError Definition -> [LocalDisplayForm])
-> m (Either SigError Definition) -> m [LocalDisplayForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q
  ds1 <- HMap.lookupDefault [] q <$> useR stImportsDisplayForms
  ds2 <- HMap.lookupDefault [] q <$> useR stImportedDisplayForms
  ifM (isLocal q) (return $ ds ++ ds1 ++ ds2)
                  (return $ ds1 ++ ds ++ ds2)

hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool
hasDisplayForms :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Bool
hasDisplayForms = ([LocalDisplayForm] -> Bool) -> m [LocalDisplayForm] -> m Bool
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool)
-> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocalDisplayForm] -> Bool
forall a. Null a => a -> Bool
null) (m [LocalDisplayForm] -> m Bool)
-> (QName -> m [LocalDisplayForm]) -> QName -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> m [LocalDisplayForm]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [LocalDisplayForm]
getDisplayForms

-- | Find all names used (recursively) by display forms of a given name.
chaseDisplayForms :: QName -> TCM (Set QName)
chaseDisplayForms :: QName -> TCM (Set QName)
chaseDisplayForms QName
q = Set QName -> [QName] -> TCM (Set QName)
go Set QName
forall a. Set a
Set.empty [QName
q]
  where
    go :: Set QName        -- Accumulator.
       -> [QName]          -- Work list.  TODO: make work set to avoid duplicate chasing?
       -> TCM (Set QName)
    go :: Set QName -> [QName] -> TCM (Set QName)
go Set QName
used []       = Set QName -> TCM (Set QName)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set QName
used
    go Set QName
used (QName
q : [QName]
qs) = do
      let rhs :: DisplayForm -> DisplayTerm
rhs (Display Int
_ Elims
_ DisplayTerm
e) = DisplayTerm
e   -- Only look at names in the right-hand side (#1870)
      let notYetUsed :: QName -> Set QName
notYetUsed QName
x = if QName
x QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
used then Set QName
forall a. Set a
Set.empty else QName -> Set QName
forall a. a -> Set a
Set.singleton QName
x
      ds <- (QName -> Set QName) -> [DisplayTerm] -> Set QName
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> Set QName
notYetUsed ([DisplayTerm] -> Set QName)
-> ([LocalDisplayForm] -> [DisplayTerm])
-> [LocalDisplayForm]
-> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocalDisplayForm -> DisplayTerm)
-> [LocalDisplayForm] -> [DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (DisplayForm -> DisplayTerm
rhs (DisplayForm -> DisplayTerm)
-> (LocalDisplayForm -> DisplayForm)
-> LocalDisplayForm
-> DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalDisplayForm -> DisplayForm
forall (t :: * -> *) a. Decoration t => t a -> a
dget)
            ([LocalDisplayForm] -> Set QName)
-> TCMT IO [LocalDisplayForm] -> TCM (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO [LocalDisplayForm]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [LocalDisplayForm]
getDisplayForms QName
q TCMT IO [LocalDisplayForm]
-> (TCErr -> TCMT IO [LocalDisplayForm])
-> TCMT IO [LocalDisplayForm]
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
`catchError_` \ TCErr
_ -> [LocalDisplayForm] -> TCMT IO [LocalDisplayForm]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])  -- might be a pattern synonym
      go (Set.union ds used) (Set.toList ds ++ qs)

-- | Check if a display form is looping.
hasLoopingDisplayForm :: QName -> TCM Bool
hasLoopingDisplayForm :: QName -> TCMT IO Bool
hasLoopingDisplayForm QName
q = QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
q (Set QName -> Bool) -> TCM (Set QName) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Set QName)
chaseDisplayForms QName
q

canonicalName :: HasConstInfo m => QName -> m QName
canonicalName :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
x = do
  def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  case def of
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c}                                -> QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> m QName) -> QName -> m QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    Record{recClause :: Defn -> Maybe Clause
recClause = Just (Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body })}    -> Maybe Term -> m QName
forall {m :: * -> *}. HasConstInfo m => Maybe Term -> m QName
can Maybe Term
body
    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just (Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body })} -> Maybe Term -> m QName
forall {m :: * -> *}. HasConstInfo m => Maybe Term -> m QName
can Maybe Term
body
    Defn
_                                                         -> QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  where
    can :: Maybe Term -> m QName
can Maybe Term
body = QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (QName -> m QName) -> QName -> m QName
forall a b. (a -> b) -> a -> b
$ Term -> QName
extract (Term -> QName) -> Term -> QName
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe Term
body
    extract :: Term -> QName
extract (Def QName
x Elims
_)  = QName
x
    extract Term
_          = QName
forall a. HasCallStack => a
__IMPOSSIBLE__

sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
sameDef :: forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d1 QName
d2 = do
  c1 <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d1
  c2 <- canonicalName d2
  if (c1 == c2) then return $ Just c1 else return Nothing

-- | Does the given constructor come from a single-constructor type?
--
-- Precondition: The name has to refer to a constructor.
singleConstructorType :: QName -> TCM Bool
singleConstructorType :: QName -> TCMT IO Bool
singleConstructorType QName
q = do
  d <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case d of
    Record {}                   -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Constructor { conData :: Defn -> QName
conData = QName
d } -> do
      di <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      return $ case di of
        Record {}                  -> Bool
True
        Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> [QName] -> Peano
forall a. Sized a => a -> Peano
natSize [QName]
cs Peano -> Peano -> Bool
forall a. Eq a => a -> a -> Bool
== Peano
1
        Defn
_                          -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> TCMT IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Signature lookup errors.
data SigError
  = SigUnknown String -- ^ The name is not in the signature; default error message.
  | SigAbstract       -- ^ The name is not available, since it is abstract.
  | SigCubicalNotErasure
    -- ^ The name is not available because it was defined in Cubical
    -- Agda, but the current language is Erased Cubical Agda, and
    -- @--erasure@ is not active.

-- | Generates an error message corresponding to
-- 'SigCubicalNotErasure' for a given 'QName'.
notSoPrettySigCubicalNotErasure :: QName -> String
notSoPrettySigCubicalNotErasure :: QName -> [Char]
notSoPrettySigCubicalNotErasure QName
q =
  [Char]
"The name " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" which was defined in Cubical " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
  [Char]
"Agda can only be used in Erased Cubical Agda if the option " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
  [Char]
"--erasure is used"

-- | Generates an error message corresponding to
-- 'SigCubicalNotErasure' for a given 'QName'.
prettySigCubicalNotErasure :: MonadPretty m => QName -> m Doc
prettySigCubicalNotErasure :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettySigCubicalNotErasure QName
q = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
  [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
  [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
  [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which was defined in Cubical Agda can only be used in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
  [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Erased Cubical Agda if the option --erasure is used"

-- | An eliminator for 'SigError'. All constructors except for
-- 'SigAbstract' are assumed to be impossible.
sigError :: (HasCallStack, MonadDebug m) => m a -> SigError -> m a
sigError :: forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
m a -> SigError -> m a
sigError m a
a = \case
  SigUnknown [Char]
s         -> [Char] -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s
  SigError
SigAbstract          -> m a
a
  SigError
SigCubicalNotErasure -> m a
forall a. HasCallStack => a
__IMPOSSIBLE__

class ( Functor m
      , Applicative m
      , Fail.MonadFail m
      , HasOptions m
      , MonadDebug m
      , MonadTCEnv m
      ) => HasConstInfo m where
  -- | Lookup the definition of a name. The result is a closed thing, all free
  --   variables have been abstracted over.
  getConstInfo :: QName -> m Definition
  getConstInfo QName
q = QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q m (Either SigError Definition)
-> (Either SigError Definition -> m Definition) -> m Definition
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> Definition -> m Definition
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
      Left (SigUnknown [Char]
err) -> [Char] -> m Definition
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
err
      Left SigError
SigAbstract      -> [Char] -> m Definition
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ ([Char] -> m Definition) -> [Char] -> m Definition
forall a b. (a -> b) -> a -> b
$
        [Char]
"Abstract, thus, not in scope: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q
      Left SigError
SigCubicalNotErasure -> [Char] -> m Definition
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ ([Char] -> m Definition) -> [Char] -> m Definition
forall a b. (a -> b) -> a -> b
$
        QName -> [Char]
notSoPrettySigCubicalNotErasure QName
q

  -- | Version that reports exceptions:
  getConstInfo' :: QName -> m (Either SigError Definition)
  -- getConstInfo' q = Right <$> getConstInfo q -- conflicts with default signature

  -- | Lookup the rewrite rules with the given head symbol.
  getRewriteRulesFor :: QName -> m RewriteRules

  -- Lifting HasConstInfo through monad transformers:

  default getConstInfo'
    :: (HasConstInfo n, MonadTrans t, m ~ t n)
    => QName -> m (Either SigError Definition)
  getConstInfo' = n (Either SigError Definition) -> m (Either SigError Definition)
n (Either SigError Definition) -> t n (Either SigError Definition)
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n (Either SigError Definition) -> m (Either SigError Definition))
-> (QName -> n (Either SigError Definition))
-> QName
-> m (Either SigError Definition)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> n (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo'

  default getRewriteRulesFor
    :: (HasConstInfo n, MonadTrans t, m ~ t n)
    => QName -> m RewriteRules
  getRewriteRulesFor = n RewriteRules -> m RewriteRules
n RewriteRules -> t n RewriteRules
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n RewriteRules -> m RewriteRules)
-> (QName -> n RewriteRules) -> QName -> m RewriteRules
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> n RewriteRules
forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor

{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}

{-# SPECIALIZE getOriginalConstInfo :: QName -> TCM Definition #-}
-- | The computation 'getConstInfo' sometimes tweaks the returned
-- 'Definition', depending on the current 'Language' and the
-- 'Language' of the 'Definition'. This variant of 'getConstInfo' does
-- not perform any tweaks.
getOriginalConstInfo ::
  (ReadTCState m, HasConstInfo m) => QName -> m Definition
getOriginalConstInfo :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo QName
q = do
  def  <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  lang <- getLanguage
  case (lang, defLanguage def) of
    (Cubical Cubical
CErased, Cubical Cubical
CFull) ->
      Lens' TCState (Maybe Cubical)
-> (Maybe Cubical -> Maybe Cubical) -> m Definition -> m Definition
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState
        ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
-> ((Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions)
-> (Maybe Cubical -> f (Maybe Cubical))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
lensOptCubical)
        (Maybe Cubical -> Maybe Cubical -> Maybe Cubical
forall a b. a -> b -> a
const (Maybe Cubical -> Maybe Cubical -> Maybe Cubical)
-> Maybe Cubical -> Maybe Cubical -> Maybe Cubical
forall a b. (a -> b) -> a -> b
$ Cubical -> Maybe Cubical
forall a. a -> Maybe a
Just Cubical
CFull)
        (QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q)
    (Language, Language)
_ -> Definition -> m Definition
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def

defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules
defaultGetRewriteRulesFor :: forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor QName
q = m Bool -> m RewriteRules -> m RewriteRules -> m RewriteRules
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> m Bool
forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
shouldReduceDef QName
q) (RewriteRules -> m RewriteRules
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []) (m RewriteRules -> m RewriteRules)
-> m RewriteRules -> m RewriteRules
forall a b. (a -> b) -> a -> b
$ do
  st <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  let sig = TCState
st TCState -> Lens' TCState Signature -> Signature
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature
      imp = TCState
st TCState -> Lens' TCState Signature -> Signature
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports
      look Signature
s = QName -> RewriteRuleMap -> Maybe RewriteRules
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q (RewriteRuleMap -> Maybe RewriteRules)
-> RewriteRuleMap -> Maybe RewriteRules
forall a b. (a -> b) -> a -> b
$ Signature
s Signature -> Lens' Signature RewriteRuleMap -> RewriteRuleMap
forall o i. o -> Lens' o i -> i
^. (RewriteRuleMap -> f RewriteRuleMap) -> Signature -> f Signature
Lens' Signature RewriteRuleMap
sigRewriteRules
  return $ mconcat $ catMaybes [look sig, look imp]

-- | Get the original name of the projection
--   (the current one could be from a module application).
getOriginalProjection :: HasConstInfo m => QName -> m QName
getOriginalProjection :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
q = Projection -> QName
projOrig (Projection -> QName)
-> (Maybe Projection -> Projection) -> Maybe Projection -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Projection -> Maybe Projection -> Projection
forall a. a -> Maybe a -> a
fromMaybe Projection
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Projection -> QName) -> m (Maybe Projection) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
q

instance HasConstInfo (TCMT IO) where
  getRewriteRulesFor :: QName -> TCMT IO RewriteRules
getRewriteRulesFor = QName -> TCMT IO RewriteRules
forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor
  getConstInfo' :: QName -> TCMT IO (Either SigError Definition)
getConstInfo' QName
q = do
    st  <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    env <- askTC
    defaultGetConstInfo st env q
  getConstInfo :: QName -> TCMT IO Definition
getConstInfo QName
q = QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO Definition)
-> TCMT IO Definition
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
      Left (SigUnknown [Char]
err)     -> [Char] -> TCMT IO Definition
forall a. [Char] -> TCMT IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
err
      Left SigError
SigAbstract          -> QName -> TCMT IO Definition
forall a. QName -> TCM a
notInScopeError (QName -> TCMT IO Definition) -> QName -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ QName -> QName
qnameToConcrete QName
q
      Left SigError
SigCubicalNotErasure ->
        TypeError -> TCMT IO Definition
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Definition)
-> (Doc -> TypeError) -> Doc -> TCMT IO Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO Definition) -> TCMT IO Doc -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettySigCubicalNotErasure QName
q

defaultGetConstInfo
  :: (HasOptions m, MonadDebug m, MonadTCEnv m)
  => TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo :: forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCEnv m) =>
TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q = do
    let defs :: Definitions
defs  = TCState
st TCState -> Lens' TCState Definitions -> Definitions
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Definitions -> f Definitions) -> Signature -> f Signature)
-> (Definitions -> f Definitions)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Signature Definitions
sigDefinitions
        idefs :: Definitions
idefs = TCState
st TCState -> Lens' TCState Definitions -> Definitions
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports   ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Definitions -> f Definitions) -> Signature -> f Signature)
-> (Definitions -> f Definitions)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Signature Definitions
sigDefinitions
    case [Maybe Definition] -> [Definition]
forall a. [Maybe a] -> [a]
catMaybes [QName -> Definitions -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
defs, QName -> Definitions -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
idefs] of
        []  -> Either SigError Definition -> m (Either SigError Definition)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> m (Either SigError Definition))
-> Either SigError Definition -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ SigError -> Either SigError Definition
forall a b. a -> Either a b
Left (SigError -> Either SigError Definition)
-> SigError -> Either SigError Definition
forall a b. (a -> b) -> a -> b
$ [Char] -> SigError
SigUnknown ([Char] -> SigError) -> [Char] -> SigError
forall a b. (a -> b) -> a -> b
$ [Char]
"Unbound name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
showQNameId QName
q
        [Definition
d] -> Definition -> m (Either SigError Definition)
forall {m :: * -> *}.
HasOptions m =>
Definition -> m (Either SigError Definition)
checkErasureFixQuantity Definition
d m (Either SigError Definition)
-> (Either SigError Definition -> m (Either SigError Definition))
-> m (Either SigError Definition)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                 Left SigError
err -> Either SigError Definition -> m (Either SigError Definition)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SigError -> Either SigError Definition
forall a b. a -> Either a b
Left SigError
err)
                 Right Definition
d  -> TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env Definition
d
        [Definition]
ds  -> [Char] -> m (Either SigError Definition)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ ([Char] -> m (Either SigError Definition))
-> [Char] -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q
    where
      mkAbs :: TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env Definition
d
        -- Apply the reducibility rules (abstract, opaque) to check
        -- whether the definition should be hidden behind an
        -- 'AbstractDef'.
        | Bool -> Bool
not (TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
st Definition
d{defName = q'}) =
          case Definition -> Maybe Definition
alwaysMakeAbstract Definition
d of
            Just Definition
d      -> Either SigError Definition -> m (Either SigError Definition)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> m (Either SigError Definition))
-> Either SigError Definition -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ Definition -> Either SigError Definition
forall a b. b -> Either a b
Right Definition
d
            Maybe Definition
Nothing     -> Either SigError Definition -> m (Either SigError Definition)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> m (Either SigError Definition))
-> Either SigError Definition -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ SigError -> Either SigError Definition
forall a b. a -> Either a b
Left SigError
SigAbstract
              -- the above can happen since the scope checker is a bit sloppy with 'abstract'
        | Bool
otherwise = Either SigError Definition -> m (Either SigError Definition)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> m (Either SigError Definition))
-> Either SigError Definition -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ Definition -> Either SigError Definition
forall a b. b -> Either a b
Right Definition
d
        where
          q' :: QName
q' = case Definition -> Defn
theDef Definition
d of
            -- Hack to make abstract constructors work properly. The constructors
            -- live in a module with the same name as the datatype, but for 'abstract'
            -- purposes they're considered to be in the same module as the datatype.
            Constructor{} -> QName -> QName
dropLastModule QName
q
            Defn
_             -> QName
q

          dropLastModule :: QName -> QName
dropLastModule q :: QName
q@QName{ qnameModule :: QName -> ModuleName
qnameModule = ModuleName
m } =
            QName
q{ qnameModule = mnameFromList $
                 initWithDefault __IMPOSSIBLE__ $ mnameToList m
             }

      -- Names defined in Cubical Agda may only be used in Erased
      -- Cubical Agda if --erasure is used. In that case they are (to
      -- a large degree) treated as erased.
      checkErasureFixQuantity :: Definition -> m (Either SigError Definition)
checkErasureFixQuantity Definition
d = do
        current <- m Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
        if defLanguage d == Cubical CFull &&
           current == Cubical CErased
        then do
          erasure <- optErasure <$> pragmaOptions
          return $
            if erasure
            then Right $ setQuantity zeroQuantity d
            else Left SigCubicalNotErasure
        else return $ Right d

-- HasConstInfo lifts through monad transformers
-- (see default signatures in HasConstInfo class).

instance HasConstInfo m => HasConstInfo (ChangeT m)
instance HasConstInfo m => HasConstInfo (ExceptT err m)
instance HasConstInfo m => HasConstInfo (IdentityT m)
instance HasConstInfo m => HasConstInfo (ListT m)
instance HasConstInfo m => HasConstInfo (MaybeT m)
instance HasConstInfo m => HasConstInfo (ReaderT r m)
instance HasConstInfo m => HasConstInfo (StateT s m)
instance (Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m)
instance HasConstInfo m => HasConstInfo (BlockT m)

{-# INLINE getConInfo #-}
getConInfo :: HasConstInfo m => ConHead -> m Definition
getConInfo :: forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo = QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (QName -> m Definition)
-> (ConHead -> QName) -> ConHead -> m Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName

-- | Look up the polarity of a definition.
getPolarity :: HasConstInfo m => QName -> m [Polarity]
getPolarity :: forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
q = Definition -> [Polarity]
defPolarity (Definition -> [Polarity]) -> m Definition -> m [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | Look up polarity of a definition and compose with polarity
--   represented by 'Comparison'.
getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]
getPolarity' :: forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq  QName
q = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
composePol Polarity
Invariant) ([Polarity] -> [Polarity]) -> m [Polarity] -> m [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
q -- return []
getPolarity' Comparison
CmpLeq QName
q = QName -> m [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
q -- composition with Covariant is identity

-- | Set the polarity of a definition.
setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m ()
setPolarity :: forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
q [Polarity]
pol = do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Setting polarity of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Polarity] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Polarity]
pol TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity (([Polarity] -> [Polarity]) -> Definition -> Definition)
-> ([Polarity] -> [Polarity]) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ [Polarity] -> [Polarity] -> [Polarity]
forall a b. a -> b -> a
const [Polarity]
pol

-- | Look up the forced arguments of a definition.
getForcedArgs :: HasConstInfo m => QName -> m [IsForced]
getForcedArgs :: forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
q = Definition -> [IsForced]
defForced (Definition -> [IsForced]) -> m Definition -> m [IsForced]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | Get argument occurrence info for argument @i@ of definition @d@ (never fails).
getArgOccurrence :: QName -> Nat -> TCM Occurrence
getArgOccurrence :: QName -> Int -> TCM Occurrence
getArgOccurrence QName
d Int
i = do
  def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  return $! case theDef def of
    Constructor{} -> Occurrence
StrictPos
    Defn
_             -> Occurrence -> Maybe Occurrence -> Occurrence
forall a. a -> Maybe a -> a
fromMaybe Occurrence
Mixed (Maybe Occurrence -> Occurrence) -> Maybe Occurrence -> Occurrence
forall a b. (a -> b) -> a -> b
$ Definition -> [Occurrence]
defArgOccurrences Definition
def [Occurrence] -> Int -> Maybe Occurrence
forall a. [a] -> Int -> Maybe a
!!! Int
i

-- | Sets the 'defArgOccurrences' for the given identifier (which
-- should already exist in the signature).
setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m ()
setArgOccurrences :: forall (m :: * -> *).
MonadTCState m =>
QName -> [Occurrence] -> m ()
setArgOccurrences QName
d [Occurrence]
os = QName -> ([Occurrence] -> [Occurrence]) -> m ()
forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d (([Occurrence] -> [Occurrence]) -> m ())
-> ([Occurrence] -> [Occurrence]) -> m ()
forall a b. (a -> b) -> a -> b
$ [Occurrence] -> [Occurrence] -> [Occurrence]
forall a b. a -> b -> a
const [Occurrence]
os

modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences :: forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d [Occurrence] -> [Occurrence]
f =
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences [Occurrence] -> [Occurrence]
f

setTreeless :: QName -> TTerm -> TCM ()
setTreeless :: QName -> TTerm -> TCM ()
setTreeless QName
q TTerm
t =
  QName -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> TCM ())
-> (Definition -> Definition) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    fun :: Defn
fun@Function{} -> Defn
fun{ funTreeless = Just $ Compiled t Nothing }
    Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()
setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()
setCompiledArgUse QName
q [ArgUsage]
use =
  QName -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> TCM ())
-> (Definition -> Definition) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    fun :: Defn
fun@Function{} ->
      Defn
fun{ funTreeless = funTreeless fun <&> \ Compiled
c -> Compiled
c { cArgUsage = Just use } }
    Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled QName
q = do
  (Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q) m Defn -> (Defn -> Maybe Compiled) -> m (Maybe Compiled)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Function{ funTreeless :: Defn -> Maybe Compiled
funTreeless = Maybe Compiled
t } -> Maybe Compiled
t
    Defn
_                           -> Maybe Compiled
forall a. Maybe a
Nothing

-- | Returns a list of length 'conArity'.
--   If no erasure analysis has been performed yet, this will be a list of 'False's.
getErasedConArgs :: HasConstInfo m => QName -> m [Bool]
getErasedConArgs :: forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
getErasedConArgs QName
q = do
  def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case theDef def of
    Constructor{ Int
conArity :: Defn -> Int
conArity :: Int
conArity, Maybe [Bool]
conErased :: Maybe [Bool]
conErased :: Defn -> Maybe [Bool]
conErased } -> [Bool] -> m [Bool]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> m [Bool]) -> [Bool] -> m [Bool]
forall a b. (a -> b) -> a -> b
$
      [Bool] -> Maybe [Bool] -> [Bool]
forall a. a -> Maybe a -> a
fromMaybe (Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
conArity Bool
False) Maybe [Bool]
conErased
    Defn
_ -> m [Bool]
forall a. HasCallStack => a
__IMPOSSIBLE__

setErasedConArgs :: QName -> [Bool] -> TCM ()
setErasedConArgs :: QName -> [Bool] -> TCM ()
setErasedConArgs QName
q [Bool]
args = QName -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> TCM ())
-> (Definition -> Definition) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    def :: Defn
def@Constructor{ Int
conArity :: Defn -> Int
conArity :: Int
conArity }
      | [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
conArity -> Defn
def{ conErased = Just args }
      | Bool
otherwise               -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
def -> Defn
def   -- no-op for non-constructors

getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm)
getTreeless :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe TTerm)
getTreeless QName
q = (Compiled -> TTerm) -> Maybe Compiled -> Maybe TTerm
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Compiled -> TTerm
cTreeless (Maybe Compiled -> Maybe TTerm)
-> m (Maybe Compiled) -> m (Maybe TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Compiled)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled QName
q

getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage])
getCompiledArgUse :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q = (Compiled -> Maybe [ArgUsage]
cArgUsage (Compiled -> Maybe [ArgUsage])
-> Maybe Compiled -> Maybe [ArgUsage]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Maybe Compiled -> Maybe [ArgUsage])
-> m (Maybe Compiled) -> m (Maybe [ArgUsage])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Compiled)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled QName
q

-- | add data constructors to a datatype
addDataCons :: QName -> [QName] -> TCM ()
addDataCons :: QName -> [QName] -> TCM ()
addDataCons QName
d [QName]
cs = (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \ Defn
def ->
  let !cs' :: [QName]
cs' = [QName]
cs [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ Defn -> [QName]
dataCons Defn
def in
  case Defn
def of
    Datatype{} -> Defn
def {dataCons = cs' }
    Defn
_          -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Get the mutually recursive identifiers of a symbol from the signature.
getMutual :: QName -> TCM (Maybe [QName])
getMutual :: QName -> TCM (Maybe [QName])
getMutual QName
d = Defn -> Maybe [QName]
getMutual_ (Defn -> Maybe [QName])
-> (Definition -> Defn) -> Definition -> Maybe [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Maybe [QName])
-> TCMT IO Definition -> TCM (Maybe [QName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d

-- | Get the mutually recursive identifiers from a `Definition`.
getMutual_ :: Defn -> Maybe [QName]
getMutual_ :: Defn -> Maybe [QName]
getMutual_ = \case
    Function {  funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
m } -> Maybe [QName]
m
    Datatype { dataMutual :: Defn -> Maybe [QName]
dataMutual = Maybe [QName]
m } -> Maybe [QName]
m
    Record   {  recMutual :: Defn -> Maybe [QName]
recMutual = Maybe [QName]
m } -> Maybe [QName]
m
    Defn
_ -> Maybe [QName]
forall a. Maybe a
Nothing

-- | Set the mutually recursive identifiers.
--
--   TODO: This produces data of quadratic size (which has to be processed upon serialization).
--   Presumably qs is usually short, but in some cases (for instance for generated code) it may be
--   long. It would be better to assign a unique identifier to each SCC, and store the names
--   separately.
setMutual :: QName -> [QName] -> TCM ()
setMutual :: QName -> [QName] -> TCM ()
setMutual QName
d [QName]
m = (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \ Defn
def ->
  case Defn
def of
    Function{} -> Defn
def { funMutual = Just m }
    Datatype{} -> Defn
def {dataMutual = Just m }
    Record{}   -> Defn
def { recMutual = Just m }
    Defn
_          -> if [QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
m then Defn
def else Defn
forall a. HasCallStack => a
__IMPOSSIBLE__ -- nothing to do

-- | Check whether two definitions are mutually recursive.
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive :: QName -> QName -> TCMT IO Bool
mutuallyRecursive QName
d QName
d1 = (QName
d QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([QName] -> Bool)
-> (Maybe [QName] -> [QName]) -> Maybe [QName] -> Bool
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] -> Bool) -> TCM (Maybe [QName]) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe [QName])
getMutual QName
d1

-- | A function/data/record definition is nonRecursive if it is not even mutually
--   recursive with itself.
definitelyNonRecursive_ :: Defn -> Bool
definitelyNonRecursive_ :: Defn -> Bool
definitelyNonRecursive_ = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False [QName] -> Bool
forall a. Null a => a -> Bool
null (Maybe [QName] -> Bool) -> (Defn -> Maybe [QName]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe [QName]
getMutual_

-- | Get the number of parameters to the current module.
getCurrentModuleFreeVars :: TCM Nat
getCurrentModuleFreeVars :: TCMT IO Int
getCurrentModuleFreeVars = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> TCMT IO Telescope -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (ModuleName -> TCMT IO Telescope)
-> TCMT IO ModuleName -> TCMT IO Telescope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)

--   For annoying reasons the qnameModule of a pattern lambda is not correct
--   (#2883), so make sure to grab the right module for those.
getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)
getDefModule :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ModuleName)
getDefModule QName
f = (Definition -> ModuleName)
-> Either SigError Definition -> Either SigError ModuleName
forall b d a. (b -> d) -> Either a b -> Either a d
mapRight Definition -> ModuleName
modName (Either SigError Definition -> Either SigError ModuleName)
-> m (Either SigError Definition) -> m (Either SigError ModuleName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
f
  where
    modName :: Definition -> ModuleName
modName Definition
def = case Definition -> Defn
theDef Definition
def of
      Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
_ Maybe System
_) } -> ModuleName
m
      Defn
_                                               -> QName -> ModuleName
qnameModule QName
f

-- | Compute the number of free variables of a defined name. This is the sum of
--   number of parameters shared with the current module and the number of
--   anonymous variables (if the name comes from a let-bound module).
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat
getDefFreeVars :: forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars = ModuleName -> m Int
forall (m :: * -> *).
(Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
ModuleName -> m Int
getModuleFreeVars (ModuleName -> m Int) -> (QName -> ModuleName) -> QName -> m Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule

freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m,
                    ReadTCState m, MonadTCEnv m, MonadDebug m)
                => QName -> m Args
freeVarsToApply :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply QName
q = do
  vs <- ModuleName -> m [Arg Term]
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> m [Arg Term]) -> ModuleName -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
  -- Andreas, 2021-07-14, issue #5470
  -- getConstInfo will fail if q is not in scope,
  -- but in this case there are no free vars to apply, since
  -- we cannot be in a child module of its defining module.
  -- So if we short cut the nil-case here, we avoid the internal error of #5470.
  if null vs then return [] else do
  t <- defType <$> getConstInfo q
  let TelV tel _ = telView'UpTo (size vs) t
  unless (size tel == size vs) __IMPOSSIBLE__
  return $ zipWith (\ Arg Term
arg Dom ([Char], Type)
dom -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg Term -> Arg ([Char], Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ([Char], Type) -> Arg ([Char], Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom ([Char], Type)
dom) vs $ telToList tel

{-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-}
getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m)
                  => ModuleName -> m Nat
getModuleFreeVars :: forall (m :: * -> *).
(Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
ModuleName -> m Int
getModuleFreeVars ModuleName
m = do
  m0   <- ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
m (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  (+) <$> getAnonymousVariables m <*> (size <$> lookupSection m0)

-- | Compute the context variables to apply a definition to.
--
--   We have to insert the module telescope of the common prefix
--   of the current module and the module where the definition comes from.
--   (Properly raised to the current context.)
--
--   Example:
--   @
--      module M₁ Γ where
--        module M₁ Δ where
--          f = ...
--        module M₃ Θ where
--          ... M₁.M₂.f [insert Γ raised by Θ]
--   @
moduleParamsToApply :: (Functor m, Applicative m, HasOptions m,
                        MonadTCEnv m, ReadTCState m, MonadDebug m)
                    => ModuleName -> m Args
moduleParamsToApply :: forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply ModuleName
m = do

  [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.sig.param" Int
90 (TCMT IO Doc
"computing module parameters of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ do

  -- Jesper, 2020-01-22: If the module parameter substitution for the
  -- module cannot be found, that likely means we are within a call to
  -- @inTopContext@. In that case we should provide no arguments for
  -- the module parameters (see #4383).
  m (Maybe Substitution)
-> m [Arg Term] -> (Substitution -> m [Arg Term]) -> m [Arg Term]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe Substitution)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe Substitution)
getModuleParameterSub ModuleName
m) ([Arg Term] -> m [Arg Term]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []) ((Substitution -> m [Arg Term]) -> m [Arg Term])
-> (Substitution -> m [Arg Term]) -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ \Substitution
sub -> do

  [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.sig.param" Int
60 (do
    cxt <- TCMT IO [ContextEntry]
forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
    nest 2 $ vcat
      [ "cxt  = " <+> prettyTCM (PrettyContext cxt)
      , "sub  = " <+> pretty sub
      ]) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ do

  -- Get the correct number of free variables (correctly raised) of @m@.
  n   <- ModuleName -> m Int
forall (m :: * -> *).
(Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
ModuleName -> m Int
getModuleFreeVars ModuleName
m
  traceSDoc "tc.sig.param" 60 (nest 2 $ "n    = " <+> text (show n)) $ do
  tel <- take n . telToList <$> lookupSection m
  traceSDoc "tc.sig.param" 60 (nest 2 $ "tel  = " <+> pretty tel) $ do
  unless (size tel == n) __IMPOSSIBLE__
  let args = Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Arg Term])
sub ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Int -> Dom ([Char], Type) -> Arg Term)
-> [Int] -> [Dom ([Char], Type)] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Dom ([Char], Type)
a -> Int -> Term
var Int
i Term -> Arg ([Char], Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ([Char], Type) -> Arg ([Char], Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom ([Char], Type)
a) (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) [Dom ([Char], Type)]
tel
  traceSDoc "tc.sig.param" 60 (nest 2 $ "args = " <+> prettyList_ (map pretty args)) $ do

  -- Apply the original ArgInfo, as the hiding information in the current
  -- context might be different from the hiding information expected by @m@.

  getSection m >>= \case
    Maybe Section
Nothing -> do
      -- We have no section for @m@.
      -- This should only happen for toplevel definitions, and then there
      -- are no free vars to apply, or?
      -- unless (null args) __IMPOSSIBLE__
      -- No, this invariant is violated by private modules, see Issue1701a.
      [Arg Term] -> m [Arg Term]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
    Just (Section Telescope
stel) -> do
      -- The section telescope of @m@ should be as least
      -- as long as the number of free vars @m@ is applied to.
      -- We still check here as in no case, we want @zipWith@ to silently
      -- drop some @args@.
      -- And there are also anonymous modules, thus, the invariant is not trivial.
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
stel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
args) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      [Arg Term] -> m [Arg Term]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> Arg Term -> Arg Term)
-> [Dom ([Char], Type)] -> [Arg Term] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ !Dom ([Char], Type)
dom (Arg ArgInfo
_ Term
v) -> Term
v Term -> Arg ([Char], Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ([Char], Type) -> Arg ([Char], Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom ([Char], Type)
dom) (Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
stel) [Arg Term]
args

-- | Unless all variables in the context are module parameters, create a fresh
--   module to capture the non-module parameters. Used when unquoting to make
--   sure generated definitions work properly.
inFreshModuleIfFreeParams :: TCM a -> TCM a
inFreshModuleIfFreeParams :: forall a. TCM a -> TCM a
inFreshModuleIfFreeParams TCM a
k = do
  msub <- ModuleName -> TCMT IO (Maybe Substitution)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe Substitution)
getModuleParameterSub (ModuleName -> TCMT IO (Maybe Substitution))
-> TCMT IO ModuleName -> TCMT IO (Maybe Substitution)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  if isNothing msub || msub == Just IdS then k else do
    m  <- currentModule
    m' <- qualifyM m . mnameFromList1 . singleton <$>
            freshName_ ("_" :: String)
    addSection m'
    withCurrentModule m' k

-- | Instantiate a closed definition with the correct part of the current
--   context.
{-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-}
instantiateDef
  :: ( Functor m, HasConstInfo m, HasOptions m
     , ReadTCState m, MonadTCEnv m, MonadDebug m )
  => Definition -> m Definition
instantiateDef :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
d = do
  vs  <- QName -> m [Arg Term]
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply (QName -> m [Arg Term]) -> QName -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
d
  verboseS "tc.sig.inst" 30 $ do
    ctx <- getContext
    m   <- currentModule
    reportSDoc "tc.sig.inst" 30 $
      "instDef in" <+> pretty m <> ":" <+> pretty (defName d) <+>
      fsep (map pretty $ zipWith (<$) (reverse $ map (fst . unDom) ctx) vs)
  return $ d `apply` vs

instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
                           ReadTCState m, MonadTCEnv m, MonadDebug m)
                       => RewriteRule -> m RewriteRule
instantiateRewriteRule :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRule -> m RewriteRule
instantiateRewriteRule RewriteRule
rew = do
  [Char] -> Int -> TCMT IO Doc -> m RewriteRule -> m RewriteRule
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"rewriting" Int
95 (TCMT IO Doc
"instantiating rewrite rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (RewriteRule -> QName
rewName RewriteRule
rew) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to the local context.") (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
forall a b. (a -> b) -> a -> b
$ do
  vs  <- QName -> m [Arg Term]
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply (QName -> m [Arg Term]) -> QName -> m [Arg Term]
forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewName RewriteRule
rew
  let rew' = RewriteRule
rew RewriteRule -> [Arg Term] -> RewriteRule
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs
  traceSLn "rewriting" 95 ("instantiated rewrite rule: ") $ do
  traceSLn "rewriting" 95 (show rew') $ do
  return rew'

instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m,
                            ReadTCState m, MonadTCEnv m, MonadDebug m)
                        => RewriteRules -> m RewriteRules
instantiateRewriteRules :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRules -> m RewriteRules
instantiateRewriteRules = (RewriteRule -> m RewriteRule) -> RewriteRules -> m RewriteRules
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 RewriteRule -> m RewriteRule
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRule -> m RewriteRule
instantiateRewriteRule

-- | Return the abstract view of a definition, /regardless/ of whether
-- the definition would be treated abstractly.
alwaysMakeAbstract :: Definition -> Maybe Definition
alwaysMakeAbstract :: Definition -> Maybe Definition
alwaysMakeAbstract Definition
d =
  do
    def <- Defn -> Maybe Defn
makeAbs (Defn -> Maybe Defn) -> Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
d
    pure d { defArgOccurrences = [] -- no positivity info for abstract things!
           , defPolarity       = [] -- no polarity info for abstract things!
           , theDef = def
           }
  where
    makeAbs :: Defn -> Maybe Defn
makeAbs d :: Defn
d@Axiom{}            = Defn -> Maybe Defn
forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@DataOrRecSig{}     = Defn -> Maybe Defn
forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@GeneralizableVar{} = Defn -> Maybe Defn
forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@Datatype {} = Defn -> Maybe Defn
forall a. a -> Maybe a
Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs d :: Defn
d@Function {} = Defn -> Maybe Defn
forall a. a -> Maybe a
Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs Constructor{} = Maybe Defn
forall a. Maybe a
Nothing
    -- Andreas, 2012-11-18:  Make record constructor and projections abstract.
    -- Andreas, 2017-08-14:  Projections are actually not abstract (issue #2682).
    -- Return the Defn under a wrapper to allow e.g. eligibleForProjectionLike
    -- to see whether the abstract thing is a record type or not.
    makeAbs d :: Defn
d@Record{}    = Defn -> Maybe Defn
forall a. a -> Maybe a
Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs Primitive{}   = Maybe Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
    makeAbs PrimitiveSort{} = Maybe Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
    makeAbs AbstractDefn{} = Maybe Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Enter abstract mode. Abstract definition in the current module are transparent.
{-# SPECIALIZE inAbstractMode :: TCM a -> TCM a #-}
inAbstractMode :: MonadTCEnv m => m a -> m a
inAbstractMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envAbstractMode = AbstractMode }

-- | Not in abstract mode. All abstract definitions are opaque.
{-# SPECIALIZE inConcreteMode :: TCM a -> TCM a #-}
inConcreteMode :: MonadTCEnv m => m a -> m a
inConcreteMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envAbstractMode = ConcreteMode }

-- | Ignore abstract mode. All abstract definitions are transparent.
ignoreAbstractMode :: MonadTCEnv m => m a -> m a
ignoreAbstractMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envAbstractMode = IgnoreAbstractMode }

-- | Go under the given opaque block. The unfolding set will turn opaque
-- definitions transparent.
{-# SPECIALIZE underOpaqueId :: OpaqueId -> TCM a -> TCM a #-}
underOpaqueId :: MonadTCEnv m => OpaqueId -> m a -> m a
underOpaqueId :: forall (m :: * -> *) a. MonadTCEnv m => OpaqueId -> m a -> m a
underOpaqueId OpaqueId
i = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envCurrentOpaqueId = Just i }

-- | Outside of any opaque blocks.
{-# SPECIALIZE notUnderOpaque :: TCM a -> TCM a #-}
notUnderOpaque :: MonadTCEnv m => m a -> m a
notUnderOpaque :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
notUnderOpaque = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envCurrentOpaqueId = Nothing }

-- | Enter the reducibility environment associated with a definition:
-- The environment will have the same concreteness as the name, and we
-- will be in the opaque block enclosing the name, if any.
{-# SPECIALIZE inConcreteOrAbstractMode :: QName -> (Definition -> TCM a) -> TCM a #-}
inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode :: forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q Definition -> m a
cont = do
  -- Andreas, 2015-07-01: If we do not ignoreAbstractMode here,
  -- we will get ConcreteDef for abstract things, as they are turned into axioms.
  def <- m Definition -> m Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m Definition -> m Definition) -> m Definition -> m Definition
forall a b. (a -> b) -> a -> b
$ QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let
    k1 = case Definition -> IsAbstract
defAbstract Definition
def of
      IsAbstract
AbstractDef -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode
      IsAbstract
ConcreteDef -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode

    k2 = case Definition -> IsOpaque
defOpaque Definition
def of
      OpaqueDef OpaqueId
i    -> OpaqueId -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => OpaqueId -> m a -> m a
underOpaqueId OpaqueId
i
      IsOpaque
TransparentDef -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
notUnderOpaque
  k2 (k1 (cont def))

-- | Get type of a constant, instantiated to the current context.
{-# SPECIALIZE typeOfConst :: QName -> TCM Type #-}
typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type
typeOfConst :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
q = Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Definition -> m Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> m Definition) -> m Definition -> m Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q)

-- | Get relevance of a constant.
{-# SPECIALIZE relOfConst :: QName -> TCM Relevance #-}
relOfConst :: HasConstInfo m => QName -> m Relevance
relOfConst :: forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
q = Definition -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Definition -> Relevance) -> m Definition -> m Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | Get modality of a constant.
{-# SPECIALIZE modalityOfConst :: QName -> TCM Modality #-}
modalityOfConst :: HasConstInfo m => QName -> m Modality
modalityOfConst :: forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
q = Definition -> Modality
forall a. LensModality a => a -> Modality
getModality (Definition -> Modality) -> m Definition -> m Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | The number of dropped parameters for a definition.
--   0 except for projection(-like) functions and constructors.
droppedPars :: Definition -> Int
droppedPars :: Definition -> Int
droppedPars Definition
d = case Definition -> Defn
theDef Definition
d of
    Axiom{}                  -> Int
0
    DataOrRecSig{}           -> Int
0
    GeneralizableVar{}       -> Int
0
    def :: Defn
def@Function{}           -> Definition -> Int
projectionArgs Definition
d
    Datatype  {dataPars :: Defn -> Int
dataPars = Int
_} -> Int
0  -- not dropped
    Record     {recPars :: Defn -> Int
recPars = Int
_} -> Int
0  -- not dropped
    Constructor{conPars :: Defn -> Int
conPars = Int
n} -> Int
n
    Primitive{}              -> Int
0
    PrimitiveSort{}          -> Int
0
    AbstractDefn{}           -> Int
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Is it the name of a record projection?
{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
isProjection :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
qn = Defn -> Maybe Projection
isProjection_ (Defn -> Maybe Projection)
-> (Definition -> Defn) -> Definition -> Maybe Projection
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Maybe Projection)
-> m Definition -> m (Maybe Projection)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn

isProjection_ :: Defn -> Maybe Projection
isProjection_ :: Defn -> Maybe Projection
isProjection_ Defn
def =
  case Defn
def of
    Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
result } -> Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
result
    Defn
_                                         -> Maybe Projection
forall a. Maybe a
Nothing

-- | Is it the name of a non-irrelevant record projection?
{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)
isRelevantProjection :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
qn = Definition -> Maybe Projection
isRelevantProjection_ (Definition -> Maybe Projection)
-> m Definition -> m (Maybe Projection)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn

isRelevantProjection_ :: Definition -> Maybe Projection
isRelevantProjection_ :: Definition -> Maybe Projection
isRelevantProjection_ Definition
def =
  if Definition -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
def then Maybe Projection
forall a. Maybe a
Nothing else Defn -> Maybe Projection
isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def

-- | Is it a function marked STATIC?
isStaticFun :: Defn -> Bool
isStaticFun :: Defn -> Bool
isStaticFun = (Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funStatic)

-- | Is it a function marked INLINE?
isInlineFun :: Defn -> Bool
isInlineFun :: Defn -> Bool
isInlineFun = (Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funInline)

-- | Returns @True@ if we are dealing with a proper projection,
--   i.e., not a projection-like function nor a record field value
--   (projection applied to argument).
isProperProjection :: Defn -> Bool
isProperProjection :: Defn -> Bool
isProperProjection Defn
d = Maybe Projection -> Bool -> (Projection -> Bool) -> Bool
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Defn -> Maybe Projection
isProjection_ Defn
d) Bool
False ((Projection -> Bool) -> Bool) -> (Projection -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ Projection
isP ->
  (Projection -> Int
projIndex Projection
isP Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) Bool -> Bool -> Bool
&& Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Projection -> Maybe QName
projProper Projection
isP)

-- | Number of dropped initial arguments of a projection(-like) function.
projectionArgs :: Definition -> Int
projectionArgs :: Definition -> Int
projectionArgs = Int -> (Projection -> Int) -> Maybe Projection -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int -> Int) -> (Projection -> Int) -> Projection -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
pred (Int -> Int) -> (Projection -> Int) -> Projection -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Projection -> Int
projIndex) (Maybe Projection -> Int)
-> (Definition -> Maybe Projection) -> Definition -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe Projection
isRelevantProjection_

-- | Check whether a definition uses copatterns.
usesCopatterns :: (HasConstInfo m, HasBuiltins m) => QName -> m Bool
usesCopatterns :: forall (m :: * -> *).
(HasConstInfo m, HasBuiltins m) =>
QName -> m Bool
usesCopatterns QName
q = Definition -> Bool
defCopatternLHS (Definition -> Bool) -> m Definition -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | Apply a function @f@ to its first argument, producing the proper
--   postfix projection if @f@ is a projection which is not irrelevant.
applyDef :: (HasConstInfo m)
         => ProjOrigin -> QName -> Arg Term -> m Term
applyDef :: forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f Arg Term
a = do
  let fallback :: m Term
fallback = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
a]
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  m (Maybe Projection) -> m Term -> (Projection -> m Term) -> m Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) m Term
fallback ((Projection -> m Term) -> m Term)
-> (Projection -> m Term) -> m Term
forall a b. (a -> b) -> a -> b
$ \ Projection
isP -> do
    if Projection -> Int
projIndex Projection
isP Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then m Term
fallback else do
      -- Get the original projection, if existing.
      if Maybe QName -> Bool
forall a. Maybe a -> Bool
isNothing (Projection -> Maybe QName
projProper Projection
isP) then m Term
fallback else do
        Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o (QName -> Elim) -> QName -> Elim
forall a b. (a -> b) -> a -> b
$ Projection -> QName
projOrig Projection
isP]