{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.Monad.Signature where

import Prelude hiding (null)

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 (MaybeT), runMaybeT  )
import Control.Monad.Trans.Identity  ( IdentityT )
import Control.Monad.Trans           ( MonadTrans, lift )

import Data.Either
import Data.Foldable                 ( for_ )
import Data.IntMap                   qualified as IntMap
import Data.List                     qualified as List
import Data.Set                      ( Set )
import Data.Set                      qualified as Set
import Data.Map                      qualified as Map
import Data.HashMap.Strict           qualified as HMap
import Data.Maybe
import Data.Text qualified as T
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS
import Mikan.Interaction.Options

import Mikan.Syntax.Scope.Trimming
import Mikan.Syntax.Scope.Base (LiveNames(..), isModuleAlive, isNameAlive)
import Mikan.Syntax.Abstract.Name
import Mikan.Syntax.Abstract (Ren, renamingSize, ScopeCopyInfo(..))
import Mikan.Syntax.Common
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Internal.Names
import Mikan.Syntax.Position

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

import Mikan.Interaction.Options.ProfileOptions qualified as Profile
import Mikan.Utils.CallStack.Base
import Mikan.Utils.Either
import Mikan.Utils.Function ( applyWhen )
import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.List1 ( List1, pattern (:|) )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.ListT
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty (Doc, prettyShow)
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.Tuple ( first, second )
import Mikan.Utils.Update
import Mikan.Utils.StrictReader qualified as Strict
import Mikan.Utils.StrictWriter qualified as Strict
import Mikan.Utils.StrictState  qualified as Strict

import Mikan.Utils.Impossible

-- | 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
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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"
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.signature" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"definition =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Definition -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Definition
d

  tel <- TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
  let tel' = KillRangeT Telescope
forall a. KillRange a => KillRangeT a
killRange KillRangeT Telescope -> KillRangeT Telescope
forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
d of
              Constructor{} -> (Dom Type -> Dom Type) -> KillRangeT Telescope
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hideExplicit Telescope
tel
              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) -> KillRangeT Telescope
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hideExplicit Telescope
tel 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 (BackendName, Type)]
-> Maybe ([Dom (BackendName, Type)], Dom (BackendName, Type))
forall a. [a] -> Maybe ([a], a)
initLast ([Dom (BackendName, Type)]
 -> Maybe ([Dom (BackendName, Type)], Dom (BackendName, Type)))
-> [Dom (BackendName, Type)]
-> Maybe ([Dom (BackendName, Type)], Dom (BackendName, Type))
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (BackendName, Type)]
forall t. Tele (Dom t) -> [Dom (BackendName, t)]
telToList Telescope
tel of
                    Maybe ([Dom (BackendName, Type)], Dom (BackendName, Type))
Nothing -> Telescope
fallback
                    Just ([Dom (BackendName, Type)]
doms, Dom (BackendName, Type)
dom) -> [Dom (BackendName, Type)] -> Telescope
telFromList ([Dom (BackendName, Type)] -> Telescope)
-> [Dom (BackendName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Dom (BackendName, Type) -> Dom (BackendName, Type))
-> [Dom (BackendName, Type)] -> [Dom (BackendName, Type)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom (BackendName, Type) -> Dom (BackendName, Type)
forall a. LensHiding a => a -> a
hideExplicit [Dom (BackendName, Type)]
doms [Dom (BackendName, Type)]
-> [Dom (BackendName, Type)] -> [Dom (BackendName, Type)]
forall a. [a] -> [a] -> [a]
++ [Dom (BackendName, 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'
  modifyingTC (stSignature . sigDefinitions) $ 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
                      , defArgOccurrences = if null (defArgOccurrences new)
                                              then defArgOccurrences old
                                              else defArgOccurrences new
                      , defPolarity       = if null (defPolarity new)
                                              then defPolarity old
                                              else defPolarity new
                      , defCompiledRep    = Map.unionWith (++)
                                              (defCompiledRep new)
                                              (defCompiledRep old)
                      }

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

addConstant' ::
  QName -> ArgInfo -> Type -> Defn -> TCM ()
addConstant' :: QName -> ArgInfo -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
info Type
t Defn
def = QName -> Definition -> TCM ()
addConstant QName
q (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
info QName
q Type
t Defn
def

-- | Set termination info of a defined function symbol.
setTerminates :: MonadTCState m => QName -> Maybe Bool -> m ()
setTerminates :: forall (m :: * -> *). MonadTCState m => QName -> Maybe Bool -> m ()
setTerminates QName
q Maybe Bool
b = ASetter' TCState Defn -> (Defn -> Defn) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) \case
  def :: Defn
def@Function{} -> Defn
def { funTerminates = b }
  def :: Defn
def@Record{}   -> Defn
def { recTerminates = 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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) ((Defn -> Defn) -> TCM ()) -> (Defn -> Defn) -> TCM ()
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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) ((Defn -> Defn) -> TCM ()) -> (Defn -> Defn) -> TCM ()
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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) ((Defn -> Defn) -> TCM ()) -> (Defn -> Defn) -> TCM ()
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 :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
  modifyingTC (stSignature . ix q) \Definition
def -> Definition
def
    Definition -> (Definition -> Definition) -> Definition
forall a b. a -> (a -> b) -> b
& (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([Clause] -> [Clause]) -> Defn -> Defn
updateFunClauses ([Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++! Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cls)
    Definition -> (Definition -> Definition) -> Definition
forall a b. a -> (a -> b) -> b
& (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
|| [Clause] -> Bool
forall (f :: * -> *). Foldable f => f Clause -> Bool
isCopatternLHS [Clause]
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 :: String -> TCM CompilerPragma
mkPragma String
s = Range -> String -> CompilerPragma
CompilerPragma (Range -> String -> CompilerPragma)
-> TCMT IO Range -> TCMT IO (String -> 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 (String -> CompilerPragma)
-> TCMT IO String -> 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
<*> String -> TCMT IO String
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
s

-- | Add a compiler pragma `{-\# COMPILE <backend> <name> <text> \#-}`
addPragma :: BackendName -> QName -> String -> TCM ()
addPragma :: BackendName -> QName -> String -> TCM ()
addPragma BackendName
b QName
q String
s = do
  pragma <- String -> TCM CompilerPragma
mkPragma String
s
  modifyingTC (stSignature . ix q) $ addCompilerPragma b pragma

getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma BackendName
backend QName
q = do
  ps <- BackendName -> Definition -> [CompilerPragma]
defCompilerPragmas BackendName
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, HasCallStack) =>
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 do
      TypeError -> TCM (Maybe CompilerPragma)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM (Maybe CompilerPragma))
-> (Doc -> TypeError) -> Doc -> TCM (Maybe CompilerPragma)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BackendName -> Doc -> TypeError
CustomBackendError BackendName
backend (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 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"Conflicting", BackendName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty BackendName
backend, TCMT IO Doc
"pragmas for", QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q, 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 = ASetter' TCState Bool -> Bool -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Bool -> Identity Bool) -> Signature -> Identity Signature)
-> ASetter' TCState Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Bool -> Identity Bool) -> Definition -> Identity Definition)
-> (Bool -> Identity Bool)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> ((Bool -> Identity Bool) -> Defn -> Identity Defn)
-> (Bool -> Identity Bool)
-> Definition
-> Identity Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionFlag -> Lens' Defn Bool
funFlag FunctionFlag
flag) Bool
val

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 = ASetter' TCState Definition -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Definition -> Identity Definition)
    -> Signature -> Identity Signature)
-> ASetter' TCState Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q) \Definition
def -> Definition
def { defInjective = True }

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

-- | Add a section to the signature.
--
--   The current context will be stored as the cumulative module parameters
--   for this section, and a module checkpoint entry will be added
--   into the module checkpoint stack.
addSection :: ModuleName -> TCM ()
addSection :: ModuleName -> TCM ()
addSection ModuleName
m = do
  tel <- TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
  addSection' m tel

addSection' :: ModuleName -> Telescope -> TCM ()
addSection' :: ModuleName -> Telescope -> TCM ()
addSection' ModuleName
m Telescope
tel = do
  let sec :: Section
sec = Telescope -> Section
Section Telescope
tel
  -- Make sure we do not overwrite an existing section!
  TCMT IO (Maybe Section) -> (Section -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (ModuleName -> TCMT IO (Maybe Section)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m) ((Section -> TCM ()) -> TCM ()) -> (Section -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ 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".
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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'
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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.
  cp <- 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
  setModuleCheckpoint m cp
  modifyingTC (stSignature . sigSections) $ Map.insert m sec

-- | 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 :: (ReadTCState m) => ModuleName -> m (Maybe Section)
getSection :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m = do
  sig  <- (TCState -> Getting Sections TCState Sections -> Sections
forall s a. s -> Getting a s a -> a
^. (Signature -> Const Sections Signature)
-> TCState -> Const Sections TCState
Lens' TCState Signature
stSignature ((Signature -> Const Sections Signature)
 -> TCState -> Const Sections TCState)
-> ((Sections -> Const Sections Sections)
    -> Signature -> Const Sections Signature)
-> Getting Sections TCState Sections
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sections -> Const Sections Sections)
-> Signature -> Const Sections 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 :: (ReadTCState m) => ModuleName -> m Telescope
lookupSection :: forall (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 -> Getting Telescope Section Telescope -> Telescope
forall s a. s -> Getting a s a -> a
^. Getting Telescope Section Telescope
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 :: * -> *).
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
-- @
--
-- Invoking @'addDisplayForms' x@ will add a display form for each copy @x@ transitively reduces to.
-- E.g. consider the following iterated module application.
-- @
--   module M0 (n : Nat) where
--     b : Bool
--     b = n > 42
--   module M1 (n : Nat) = M0 (suc n)
--   module M2 (n : Nat) = M1 (suc n)
--   module M3 (n : Nat) = M2 (suc n)
-- @
--
-- For the first copy @M1.b n = M0.b (suc n)@ we add the display form @M0.b (suc n) --> M1.b n@.
--
-- For the second copy @M2.b n = M1.b (suc n)@ we first add display form @M1.b (suc n) --> M2.b n@
-- and for the further unfolding we add display form @M0.b (suc (suc n)) --> M2.b n@.
--
-- For the third copy @M3.b n = M2.b (suc n)@ we add display forms @M2.b (suc n) --> M3.b n@,
-- @M1.b (suc (suc n)) --> M3.b n@ and @M0.b (suc (suc (suc n))) --> M3.b n@.

addDisplayForms :: QName -> TCM ()
addDisplayForms :: QName -> TCM ()
addDisplayForms QName
x = do
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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, HasCallStack) =>
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
  reportSDoc "tc.display.section" 20 $ "Added display forms for" <+> pretty x

  where

    -- To get display forms for projections we need to unSpine here.
    view :: Term -> ([Arg ArgName], Term)
    view :: Term -> ([Arg BackendName], Term)
view = (Term -> Term)
-> ([Arg BackendName], Term) -> ([Arg BackendName], Term)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Term -> Term
unSpine (([Arg BackendName], Term) -> ([Arg BackendName], Term))
-> (Term -> ([Arg BackendName], Term))
-> Term
-> ([Arg BackendName], Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ([Arg BackendName], 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 BackendName], Term)
view Term
v of
        ([Arg BackendName]
xs, Def QName
y Elims
es)   -> (QName
y,)         (DisplayForm -> (QName, DisplayForm))
-> DisplayForm -> (QName, DisplayForm)
forall a b. (a -> b) -> a -> b
$ [Arg BackendName] -> Elims -> DisplayForm
mkDisplay [Arg BackendName]
xs Elims
es
        ([Arg BackendName]
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 BackendName] -> Elims -> DisplayForm
mkDisplay [Arg BackendName]
xs Elims
es
        ([Arg BackendName], Term)
_ -> (QName, DisplayForm)
forall a. HasCallStack => a
__IMPOSSIBLE__
      where
        mkDisplay :: [Arg BackendName] -> Elims -> DisplayForm
mkDisplay [Arg BackendName]
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 BackendName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg BackendName]
xs
            args :: [Arg Term]
args = (Arg BackendName -> Int -> Arg Term)
-> [Arg BackendName] -> [Int] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg BackendName
x Int
i -> Int -> Term
var Int
i Term -> Arg BackendName -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg BackendName
x) [Arg BackendName]
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 BackendName], Term)
view Term
v of
      ([Arg BackendName]
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 BackendName] -> Term -> Term
unlamView [Arg BackendName]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM QName
f Elims
es)
      ([Arg BackendName]
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 BackendName] -> Term -> Term
unlamView [Arg BackendName]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM (ConHead -> QName
conName ConHead
c) Elims
es)
      ([Arg BackendName], 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 BackendName], Term) -> Term
forall a b. (a, b) -> b
snd (([Arg BackendName], Term) -> Term)
-> ([Arg BackendName], Term) -> Term
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg BackendName], 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.
            String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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 -> TCMT IO Bool -> TCM [Term] -> TCM [Term] -> TCM [Term]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Maybe QName -> Bool)
-> (Definition -> Maybe QName) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe QName
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, HasCallStack) =>
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 info :: ScopeCopyInfo
info@ScopeCopyInfo{ renModules :: ScopeCopyInfo -> Ren ModuleName
renModules = Ren ModuleName
rm, renNames :: ScopeCopyInfo -> Ren QName
renNames = Ren QName
rd } = do
  (deleted, info@ScopeCopyInfo{ renModules = rm, renNames = rd }) <- ModuleName -> ScopeCopyInfo -> TCM (Ren QName, ScopeCopyInfo)
onlyLiveCopies ModuleName
new ScopeCopyInfo
info
  rd <- closeConstructors deleted rd
  applySection' new ptel old ts info{ 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.
    --
    -- If a proper projection is being copied, its record needs to be
    -- copied too (#8037).
    closeConstructors :: Ren QName -> Ren QName -> TCM (Ren QName)
    closeConstructors :: Ren QName -> Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
del Ren QName
rd = do
        let defs :: [(QName, List1 QName)]
defs = Ren QName -> [(QName, List1 QName)]
forall k a. Map k a -> [(k, a)]
Map.toList Ren QName
rd
        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))
childToParent [(QName, List1 QName)]
defs
        cs <- nubOn snd . concat    <$> traverse parentToChild defs
        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
          -- If the name got pruned by liveness, but we're going to add
          -- it back, then we might as well add it back with the
          -- original renaming.
          | Just List1 QName
n <- QName -> Ren QName -> Maybe (List1 QName)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x Ren QName
del = Ren QName -> TCM (Ren QName)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> List1 QName -> Ren QName
forall k a. k -> a -> Map k a
Map.singleton QName
x List1 QName
n)
          | 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
<$> BackendName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => BackendName -> m Name
freshName_ (Name -> BackendName
nameToArgName (Name -> BackendName) -> Name -> BackendName
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)

        childToParent :: (QName, List1 QName) -> TCM (Maybe (ModuleName, QName))
        childToParent :: (QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName))
childToParent (QName
x, QName
y :| [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, HasCallStack) =>
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
            -- the constructors and the data type live in the same
            -- module, so it suffices to use the same module name that
            -- the constructor ended up in for the data type
            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)

            -- If a proper projection is being copied, its record needs to be
            -- copied too (#8037).
            --
            -- #8242: copying a proper projection M.R.proj → N.R.proj does not
            -- mean we should copy the record type M.R to N.R.R!
            Defn
def | Just Projection{ projProper :: Projection -> Maybe QName
projProper = Just QName
r } <- Defn -> Maybe Projection
isProjectionDefn Defn
def ->
              let
                -- putting the record in the parent of where the
                -- projection ended up seems robust. i don't think it's
                -- possible for a copied proper projection to end up
                -- nested relative to the correct place to put the
                -- record.
                parent :: ModuleName
parent = case [Name] -> Maybe ([Name], Name)
forall a. [a] -> Maybe ([a], a)
initLast (ModuleName -> [Name]
mnameToList (QName -> ModuleName
qnameModule QName
y)) of
                  Just ([Name]
mod, Name
_) -> [Name] -> ModuleName
mnameFromList [Name]
mod
                  Maybe ([Name], Name)
Nothing       -> ModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__
              in (ModuleName, QName) -> Maybe (ModuleName, QName)
forall a. a -> Maybe a
Just ([Name] -> ModuleName
mnameFromList ([Name] -> [Name]
forall a. HasCallStack => [a] -> [a]
init (ModuleName -> [Name]
mnameToList (QName -> ModuleName
qnameModule QName
y))), QName
r)

            Defn
_ -> Maybe (ModuleName, QName)
forall a. Maybe a
Nothing

        parentToChild :: (QName, List1 QName) -> TCM [(ModuleName, QName)]
        parentToChild :: (QName, List1 QName) -> TCMT IO [(ModuleName, QName)]
parentToChild (QName
x, QName
y :| [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, HasCallStack) =>
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

            -- note about the module here: the record constructor lives
            -- outside the record module, in the same module as the
            -- record.
            --
            -- in debugging output, if the record being copied has a
            -- generated constructor name, it's going to look like we
            -- accidentally lost a layer of quantification, but that's
            -- because record constructors get generated with a concrete
            -- name that *looks* qualified
            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 ren :: ScopeCopyInfo
ren@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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (QName -> TypeError
TriedToCopyConstrainedPrim QName
q)

  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
    , TCMT IO Doc
"ren  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ScopeCopyInfo -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ScopeCopyInfo
ren
    ]

  ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Sections do
    oldn <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
old

    let
      ds = Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ Ren QName -> Int
forall a. Ren a -> Int
renamingSize Ren QName
rd
      ms = Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ Ren ModuleName -> Int
forall a. Ren a -> Int
renamingSize Ren ModuleName
rm

    tickMax "largest copied section" (ds + ms)
    tickN   "copied definitions"     ds
    tickN   ("copies for " <> oldn)  (ds + ms)

  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.mod.apply" Int
40 String
"applySection': copying definitions"
  _ <- (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

  reportSLn "tc.mod.apply" 40 "applySection': copying modules"
  _ <- Map.traverseWithKey (traverse . copySec ts) rm

  reportSLn "tc.mod.apply" 40 "applySection': computing polarities"
  computePolarity (Map.elems rd >>= List1.toList)

  reportSLn "tc.mod.apply" 40 "finished applySection'"
  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
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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 :: * -> *). 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
      np  <- argsToUse (qnameModule x)
      origTel <- lookupSection $ 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.
      let hidings = (Dom (BackendName, Type) -> Hiding)
-> [Dom (BackendName, Type)] -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map Dom (BackendName, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ([Dom (BackendName, Type)] -> [Hiding])
-> [Dom (BackendName, Type)] -> [Hiding]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (BackendName, Type)]
forall t. Tele (Dom t) -> [Dom (BackendName, t)]
telToList Telescope
origTel
      -- This 'zipWith' sometimes silently drops arguments, see #8443
      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' ]
      copyDef' ts' np def
      reportSDoc "tc.mod.apply" 80 $
        "finished copyDef" <+> pretty x <+> "->" <+> pretty y
      where
        copyDef' :: [Arg Term] -> Int -> Definition -> TCM ()
copyDef' [Arg Term]
ts Int
np Definition
d = do
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
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
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (IsAbstract -> String
forall a. Show a => a -> String
show (IsAbstract -> String) -> IsAbstract -> String
forall a b. (a -> b) -> a -> b
$ Definition -> IsAbstract
defAbstract Definition
d)
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
<+> [Arg Term] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [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) ]
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
-> Bool -> Maybe InstanceInfo -> KwRange -> QName -> Type -> TCM ()
addTypedInstance' Bool
False Bool
False Maybe InstanceInfo
inst KwRange
forall a. Null a => a
empty 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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'
            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.
              TCMT IO Defn
def TCMT IO Defn -> (Defn -> Definition) -> TCMT IO Definition
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \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
                , 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 :: Map BackendName [CompilerPragma]
defCompiledRep       = Map BackendName [CompilerPragma]
noCompiledRep
                , defInstance :: Maybe InstanceInfo
defInstance          = Maybe InstanceInfo
inst
                , defCopy :: Maybe QName
defCopy              = QName -> Maybe QName
forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
d)
                , defNoCompilation :: Bool
defNoCompilation     = Definition -> Bool
defNoCompilation Definition
d
                , defInjective :: Bool
defInjective         = Bool
False
                , defCopatternLHS :: Bool
defCopatternLHS     = [Clause] -> Bool
forall (f :: * -> *). Foldable f => f Clause -> Bool
isCopatternLHS [Clause
cl]
                , defBlocked :: Blocked_
defBlocked           = Definition -> Blocked_
defBlocked Definition
d
                , defMightContainMetas :: Bool
defMightContainMetas = Bool
True
                , 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 :: WithFunInfo
with   = case Defn
oldDef of
              Function{funWith :: Defn -> WithFunInfo
funWith = WithFunInfo QName
parent Telescope
delta1 Int
nargs } -> WithFunInfo
                { wfParent :: QName
wfParent   = QName -> QName
copyName QName
parent
                , wfDelta1 :: Telescope
wfDelta1   = Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
apply Telescope
delta1 [Arg Term]
ts'
                , wfWithArgs :: Int
wfWithArgs = Int
nargs
                }
              Defn
_ -> WithFunInfo
NotWithFunction

            -- 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
                         }
                GeneralizableVar NumGeneralizableArgs
gv -> 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
$ NumGeneralizableArgs -> Defn
GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
forall a b. (a -> b) -> a -> b
$ NumGeneralizableArgs
gv NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
                Defn
_ -> do
                  (mst, _, cc) <- Maybe (Telescope, QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (Telescope, QName, Type)
forall a. Maybe a
Nothing [Clause
cl] -- Andreas, 2012-10-07 non need for record pattern translation
                  let fun = FunctionData
emptyFunctionData
                  let newDef =
                        ((Bool -> Identity Bool) -> Defn -> Identity Defn)
-> Bool -> Defn -> Defn
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> Defn -> Identity Defn
Lens' Defn Bool
funProj   (Defn
oldDef Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funProj) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        ((Bool -> Identity Bool) -> Defn -> Identity Defn)
-> Bool -> Defn -> Defn
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> Defn -> Identity Defn
Lens' Defn Bool
funMacro  (Defn
oldDef Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funMacro) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        ((Bool -> Identity Bool) -> Defn -> Identity Defn)
-> Bool -> Defn -> Defn
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> Defn -> Identity 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 -> [Arg Term] -> Term
projDropParsApply Projection
p ProjOrigin
ProjSystem [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 :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
                        , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive -- 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

    {- 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
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.mod.apply" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Copying 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
x 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
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
y
      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 $ "  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 (TS.unpack . fst . unDom) $ telToList tel))  -- only names
      reportSDoc "tc.mod.apply" 80 $ "  sectionTel   = " <+> text (unwords $ (map (TS.unpack . fst . unDom) $ telToList ptel)) -- only names
      ctxTel <- getContextTelescope
      addSection' y (ctxTel `abstract` sectionTel)
      reportSDoc "tc.mod.apply" 80 $
        "finished copySec" <+> pretty x <+> "->" <+> pretty 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
  -- Check whether display form is recursive and thus illegal.
  xs <- DisplayForm -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms DisplayForm
df Set QName
forall a. Set a
Set.empty
  if x `Set.member` xs then warning $ InvalidDisplayForm x "it is recursive" else do
  d <- makeOpen df
  let add Definition
def = Definition
def{ defDisplay = d:defDisplay def }
  ifM (isLocal x)
    {-then-} (modifyingTC (stSignature . ix x) add)
    {-else-} (stImportsDisplayForms `modifyingTC` HMap.insertWith (<>) x (List1.singleton d))
  reportSDoc "tc.display.section" 30 $ "Added 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, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q
  ds1 <- List1.toList' . HMap.lookup q <$> useR stImportsDisplayForms
  ds2 <- List1.toList' . HMap.lookup 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.
--
class ChaseDisplayForms a where
  chaseDisplayForms ::
       a                 -- ^ Search this recursively for display form names.
    -> Set QName         -- ^ Already processed names (accumulator).
    -> TCM (Set QName)   -- ^ Found names (superset of accumulator)

instance ChaseDisplayForms QName where
  chaseDisplayForms :: QName -> Set QName -> TCM (Set QName)
chaseDisplayForms QName
q Set QName
used
    | QName
q QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
used = Set QName -> TCM (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
used
    | Bool
otherwise           = do
        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.display.recursive" Int
90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"Chasing display form", QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q, TCMT IO Doc
"with accumulator", [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM (Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
used) ]
        xs <- 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_` TCMT IO [LocalDisplayForm] -> TCErr -> TCMT IO [LocalDisplayForm]
forall a b. a -> b -> a
const ([LocalDisplayForm] -> TCMT IO [LocalDisplayForm]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])  -- might be a pattern synonym
        chaseDisplayForms xs (Set.insert q used)

instance ChaseDisplayForms DisplayTerm where
  chaseDisplayForms :: DisplayTerm -> Set QName -> TCM (Set QName)
chaseDisplayForms DisplayTerm
e Set QName
used = do
    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
    let ds :: Set QName
ds = (QName -> Set QName) -> DisplayTerm -> Set QName
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> Set QName
notYetUsed DisplayTerm
e
    Set QName -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms Set QName
ds Set QName
used

instance ChaseDisplayForms DisplayForm where
  -- Only look at names in the right-hand side (#1870)
  chaseDisplayForms :: DisplayForm -> Set QName -> TCM (Set QName)
chaseDisplayForms = DisplayTerm -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms (DisplayTerm -> Set QName -> TCM (Set QName))
-> (DisplayForm -> DisplayTerm)
-> DisplayForm
-> Set QName
-> TCM (Set QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForm -> DisplayTerm
dfRHS

instance ChaseDisplayForms a => ChaseDisplayForms (Open a) where
  chaseDisplayForms :: Open a -> Set QName -> TCM (Set QName)
chaseDisplayForms = a -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms (a -> Set QName -> TCM (Set QName))
-> (Open a -> a) -> Open a -> Set QName -> TCM (Set QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Open a -> a
forall a. Open a -> a
openThing

instance ChaseDisplayForms a => ChaseDisplayForms (Set a) where
  chaseDisplayForms :: Set a -> Set QName -> TCM (Set QName)
chaseDisplayForms Set a
s = case Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set a
s of
    Maybe (a, Set a)
Nothing      -> Set QName -> TCM (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
    Just (a
x, Set a
s') -> a -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms a
x (Set QName -> TCM (Set QName))
-> (Set QName -> TCM (Set QName)) -> Set QName -> TCM (Set QName)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Set a -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms Set a
s'

instance ChaseDisplayForms a => ChaseDisplayForms [a] where
  chaseDisplayForms :: [a] -> Set QName -> TCM (Set QName)
chaseDisplayForms []     = Set QName -> TCM (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  chaseDisplayForms (a
x:[a]
xs) = a -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms a
x (Set QName -> TCM (Set QName))
-> (Set QName -> TCM (Set QName)) -> Set QName -> TCM (Set QName)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [a] -> Set QName -> TCM (Set QName)
forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
chaseDisplayForms [a]
xs
  -- NB: The following does not work because of lacking instance Ord LocalDisplayForm:
  -- chaseDisplayForms = chaseDisplayForms . Set.toList


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, HasCallStack) =>
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, HasCallStack) =>
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, HasCallStack) =>
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.

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

class ( Functor m
      , Applicative 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 :: HasCallStack => QName -> m Definition
  getConstInfo QName
q =
    QName -> m (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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 SigError
err -> (m Definition -> SigError -> m Definition)
-> SigError -> m Definition -> m Definition
forall a b c. (a -> b -> c) -> b -> a -> c
flip (QName -> m Definition -> SigError -> m Definition
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
QName -> m a -> SigError -> m a
sigError QName
q) SigError
err (m Definition -> m Definition) -> m Definition -> m Definition
forall a b. (a -> b) -> a -> b
$
        String -> m Definition
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (String -> m Definition) -> String -> m Definition
forall a b. (a -> b) -> a -> b
$
        String
"Abstract, thus, not in scope: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q

  -- | Version that reports exceptions:
  getConstInfo' :: HasCallStack => QName -> m (Either SigError Definition)

  -- Lifting HasConstInfo through monad transformers:
  default getConstInfo'
    :: (HasCallStack, 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, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo'
{-# SPECIALIZE getConstInfo :: HasCallStack => QName -> TCM Definition #-}

{-# SPECIALIZE getOriginalConstInfo :: HasCallStack => 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 :: (HasCallStack, HasConstInfo m) => QName -> m Definition
getOriginalConstInfo :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo QName
q = QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q

-- | Get the original name of the projection
--   (the current one could be from a module application).
getOriginalProjection :: (HasCallStack, HasConstInfo m) => QName -> m QName
getOriginalProjection :: forall (m :: * -> *).
(HasCallStack, 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 TCM where
  getConstInfo' :: HasCallStack => QName -> TCM (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 :: HasCallStack => QName -> TCMT IO Definition
getConstInfo QName
q = QName -> TCM (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q TCM (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 String
err)     -> String -> TCMT IO Definition
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
internalError String
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

defaultGetConstInfo
  :: (HasCallStack, HasOptions m, MonadDebug m)
  => TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo :: forall (m :: * -> *).
(HasCallStack, HasOptions m, MonadDebug m) =>
TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q = do
    let defs :: Definitions
defs  = TCState
st TCState -> Getting Definitions TCState Definitions -> Definitions
forall s a. s -> Getting a s a -> a
^. (Signature -> Const Definitions Signature)
-> TCState -> Const Definitions TCState
Lens' TCState Signature
stSignature ((Signature -> Const Definitions Signature)
 -> TCState -> Const Definitions TCState)
-> ((Definitions -> Const Definitions Definitions)
    -> Signature -> Const Definitions Signature)
-> Getting Definitions TCState Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> Const Definitions Definitions)
-> Signature -> Const Definitions Signature
Lens' Signature Definitions
sigDefinitions
        idefs :: Definitions
idefs = TCState
st TCState -> Getting Definitions TCState Definitions -> Definitions
forall s a. s -> Getting a s a -> a
^. (Signature -> Const Definitions Signature)
-> TCState -> Const Definitions TCState
Lens' TCState Signature
stImports   ((Signature -> Const Definitions Signature)
 -> TCState -> Const Definitions TCState)
-> ((Definitions -> Const Definitions Definitions)
    -> Signature -> Const Definitions Signature)
-> Getting Definitions TCState Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> Const Definitions Definitions)
-> Signature -> Const Definitions Signature
Lens' Signature Definitions
sigDefinitions
    case (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
      (Maybe Definition
Nothing, 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 -> Either SigError Definition)
-> SigError -> Either SigError Definition
forall a b. (a -> b) -> a -> b
$ String -> SigError
SigUnknown (String -> SigError) -> String -> SigError
forall a b. (a -> b) -> a -> b
$ String
"Unbound name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
showQNameId QName
q
      (Just Definition
d, Maybe Definition
Nothing)  -> TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env Definition
d
      (Maybe Definition
Nothing, Just Definition
d)  -> TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env Definition
d
      (Maybe Definition, Maybe Definition)
_                  -> String -> m (Either SigError Definition)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (String -> m (Either SigError Definition))
-> String -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ String
"Ambiguous name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
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) =
          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

-- 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 (Strict.ReaderT r m)
instance HasConstInfo m => HasConstInfo (Strict.StateT s m)
instance (Monoid w, HasConstInfo m) => HasConstInfo (Strict.WriterT w m)
instance HasConstInfo m => HasConstInfo (BlockT m)

{-# INLINE getConInfo #-}
getConInfo :: (HasCallStack, HasConstInfo m) => ConHead -> m Definition
getConInfo :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
ConHead -> m Definition
getConInfo = QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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

{-# INLINE getPolarity #-}
-- | Look up the polarity of a definition.
getPolarity :: (HasCallStack, HasConstInfo m) => QName -> m [Polarity]
getPolarity :: forall (m :: * -> *).
(HasCallStack, 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q

-- | Look up polarity of a definition and compose with polarity
--   represented by 'Comparison'.
getPolarity' :: (HasCallStack, HasConstInfo m) => Comparison -> QName -> m [Polarity]
getPolarity' :: forall (m :: * -> *).
(HasCallStack, 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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m [Polarity]
getPolarity QName
q -- return []
getPolarity' Comparison
CmpLeq QName
q = QName -> m [Polarity]
forall (m :: * -> *).
(HasCallStack, 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
  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
"."
  ASetter' TCState Definition -> (Definition -> Definition) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Definition -> Identity Definition)
    -> Signature -> Identity Signature)
-> ASetter' TCState Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q) ((Definition -> Definition) -> m ())
-> (Definition -> Definition) -> m ()
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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q

-- | Get argument occurrence info for argument @i@ of definition @d@ (never fails).
getArgOccurrence :: HasCallStack => QName -> Nat -> TCM Occurrence
getArgOccurrence :: HasCallStack => QName -> Int -> TCM Occurrence
getArgOccurrence QName
d Int
i = do
  def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
  case theDef def of
    Constructor{} -> Occurrence -> TCM Occurrence
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
StrictPos

    -- If the polarity checker has filled in the positivities of
    -- arguments for this function then we believe it, because it should
    -- agree with the signature.
    Defn
_ | Just Occurrence
pol <- Definition -> [Occurrence]
defArgOccurrences Definition
def [Occurrence] -> Int -> Maybe Occurrence
forall a. [a] -> Int -> Maybe a
!!! Int
i ->
      Occurrence -> TCM Occurrence
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
pol

    -- Otherwise we default to Mixed.
    Defn
_ -> Occurrence -> TCM Occurrence
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Mixed

-- | 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 =
  ASetter' TCState Definition -> (Definition -> Definition) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Definition -> Identity Definition)
    -> Signature -> Identity Signature)
-> ASetter' TCState Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
d) ((Definition -> Definition) -> m ())
-> (Definition -> Definition) -> m ()
forall a b. (a -> b) -> a -> b
$ ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences [Occurrence] -> [Occurrence]
f

getArgOccurrences :: ReadTCState m => QName -> m [Occurrence]
getArgOccurrences :: forall (m :: * -> *). ReadTCState m => QName -> m [Occurrence]
getArgOccurrences QName
q = Getter TCState (Maybe Definition) -> m (Maybe Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Maybe Definition -> f (Maybe Definition))
    -> Signature -> f Signature)
-> (Maybe Definition -> f (Maybe Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Lens' Signature (Maybe (IxValue Signature))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Signature
QName
q) m (Maybe Definition)
-> (Maybe Definition -> [Occurrence]) -> m [Occurrence]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
  Maybe Definition
Nothing  -> [Occurrence]
forall a. HasCallStack => a
__IMPOSSIBLE__
  Just Definition
def -> Definition -> [Occurrence]
defArgOccurrences Definition
def

-- | add data constructors to a datatype
addDataCons :: QName -> [QName] -> TCM ()
addDataCons :: QName -> [QName] -> TCM ()
addDataCons QName
d [QName]
cs = ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
d ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) \ 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, HasCallStack) =>
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 = ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
d ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) \ 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, or record definition is definitely not recursive 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 :: * -> *). 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, HasCallStack) =>
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 :: (ReadTCState m, MonadTCEnv m) => QName -> m Nat
getDefFreeVars :: forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars = ModuleName -> m Int
forall (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 :: (HasConstInfo m,
                    ReadTCState m)
                => QName -> m Args
freeVarsToApply :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Arg Term]
freeVarsToApply = ModuleName -> m [Arg Term]
forall (m :: * -> *).
(HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> m [Arg Term])
-> (QName -> ModuleName) -> QName -> m [Arg Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule

{-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-}
getModuleFreeVars :: ( MonadTCEnv m, ReadTCState m)
                  =>ModuleName -> m Nat
getModuleFreeVars :: forall (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 :: ( HasOptions m,
                        MonadTCEnv m, ReadTCState m, MonadDebug m)
                    =>ModuleName -> m Args
moduleParamsToApply :: forall (m :: * -> *).
(HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply ModuleName
m = do

  String -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"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

  String -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.sig.param" Int
60 (do
    cxt <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
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 :: * -> *).
(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 (BackendName, Type) -> Arg Term)
-> [Int] -> [Dom (BackendName, Type)] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Dom (BackendName, Type)
a -> Int -> Term
var Int
i Term -> Arg (BackendName, Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (BackendName, Type) -> Arg (BackendName, Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom (BackendName, Type)
a) (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) [Dom (BackendName, 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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 (BackendName, Type) -> Arg Term -> Arg Term)
-> [Dom (BackendName, Type)] -> [Arg Term] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ !Dom (BackendName, Type)
dom (Arg ArgInfo
_ Term
v) -> Term
v Term -> Arg (BackendName, Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (BackendName, Type) -> Arg (BackendName, Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom (BackendName, Type)
dom) (Telescope -> [Dom (BackendName, Type)]
forall t. Tele (Dom t) -> [Dom (BackendName, 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_ ("_" :: ShortText)
    addSection m'
    withCurrentModule m' k

-- | Instantiate a closed definition with the correct part of the current
--   context.
{-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-}
instantiateDef
  :: (HasConstInfo m, ReadTCState m )
  => Definition -> m Definition
instantiateDef :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
Definition -> m Definition
instantiateDef Definition
d = do
  vs  <- QName -> m [Arg Term]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState 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 <- getContextNames
    m   <- currentModule
    reportSDoc "tc.sig.inst" 30 $
      "instDef in" <+> pretty m <> ":" <+> pretty (defName d) <+>
      fsep (map pretty vs)
  return $ d `apply` vs

-- | 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 (ASetter TCEnv TCEnv AbstractMode AbstractMode
-> AbstractMode -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv AbstractMode AbstractMode
Lens' TCEnv AbstractMode
eAbstractMode AbstractMode
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 (ASetter TCEnv TCEnv AbstractMode AbstractMode
-> AbstractMode -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv AbstractMode AbstractMode
Lens' TCEnv AbstractMode
eAbstractMode AbstractMode
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 (ASetter TCEnv TCEnv AbstractMode AbstractMode
-> AbstractMode -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv AbstractMode AbstractMode
Lens' TCEnv AbstractMode
eAbstractMode AbstractMode
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 (ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
-> Maybe OpaqueId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
Lens' TCEnv (Maybe OpaqueId)
eCurrentOpaqueId (OpaqueId -> Maybe OpaqueId
forall a. a -> Maybe a
Just OpaqueId
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 (ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
-> Maybe OpaqueId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
Lens' TCEnv (Maybe OpaqueId)
eCurrentOpaqueId Maybe OpaqueId
forall a. Maybe a
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 :: (HasConstInfo m) => QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode :: forall (m :: * -> *) a.
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, HasCallStack) =>
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 :: * -> *).
(HasConstInfo m, ReadTCState 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, HasCallStack) =>
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
0 -- not impossible when quoting, PR #7828

-- | Is it the name of a record projection or field or a projection-like function?
{-# 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 = Definition -> Maybe Projection
isProjectionDefinition (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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
qn

-- | Is it a record projection or field or a projection-like function?
isProjectionDefn :: Defn -> Maybe Projection
isProjectionDefn :: Defn -> Maybe Projection
isProjectionDefn = \case
    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 a record projection or field or a projection-like function?
isProjectionDefinition :: Definition -> Maybe Projection
isProjectionDefinition :: Definition -> Maybe Projection
isProjectionDefinition = Defn -> Maybe Projection
isProjectionDefn (Defn -> Maybe Projection)
-> (Definition -> Defn) -> Definition -> Maybe Projection
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef

-- | Is it a function marked INLINE?
isInlineFun :: Defn -> Bool
isInlineFun :: Defn -> Bool
isInlineFun = (Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
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 = Bool -> (Projection -> Bool) -> Maybe Projection -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Projection -> Bool
isProperProjection_ (Maybe Projection -> Bool)
-> (Defn -> Maybe Projection) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe Projection
isProjectionDefn

-- | 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_ :: Projection -> Bool
isProperProjection_ :: Projection -> Bool
isProperProjection_ 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
isProjectionDefinition

-- | Check whether a definition uses copatterns.
usesCopatterns :: (HasConstInfo m) => QName -> m Bool
usesCopatterns :: forall (m :: * -> *). HasConstInfo 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q

-- | Apply a function @f@ to its first argument, producing the proper
--   postfix projection if @f@ is a projection.
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]
  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)
isProjection 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]