{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Monad.Signature where

import Prelude hiding (null)

import qualified Control.Monad.Fail as Fail

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

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

import Agda.Interaction.Options

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

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

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

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Update

import Agda.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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.signature" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"adding constant " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" to signature"
  Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let tel' :: Telescope
tel' = VerboseKey -> Telescope -> Telescope
forall a. VerboseKey -> Tele a -> Tele a
replaceEmptyName VerboseKey
"r" (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope
forall a. KillRange a => KillRangeT a
killRange (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
d of
              Constructor{} -> (Dom Type -> Dom Type) -> Telescope -> Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hideOrKeepInstance Telescope
tel
              Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projIndex :: Projection -> VerboseLevel
projIndex = VerboseLevel
n } } ->
                let fallback :: Telescope
fallback = (Dom Type -> Dom Type) -> Telescope -> Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hideOrKeepInstance Telescope
tel in
                if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then Telescope
fallback else
                -- if the record value is part of the telescope, its hiding should left unchanged
                  case [Dom (VerboseKey, Type)]
-> Maybe ([Dom (VerboseKey, Type)], Dom (VerboseKey, Type))
forall a. [a] -> Maybe ([a], a)
initLast ([Dom (VerboseKey, Type)]
 -> Maybe ([Dom (VerboseKey, Type)], Dom (VerboseKey, Type)))
-> [Dom (VerboseKey, Type)]
-> Maybe ([Dom (VerboseKey, Type)], Dom (VerboseKey, Type))
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel of
                    Maybe ([Dom (VerboseKey, Type)], Dom (VerboseKey, Type))
Nothing -> Telescope
fallback
                    Just ([Dom (VerboseKey, Type)]
doms, Dom (VerboseKey, Type)
dom) -> [Dom (VerboseKey, Type)] -> Telescope
telFromList ([Dom (VerboseKey, Type)] -> Telescope)
-> [Dom (VerboseKey, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Dom (VerboseKey, Type))
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom (VerboseKey, Type) -> Dom (VerboseKey, Type)
forall a. LensHiding a => a -> a
hideOrKeepInstance [Dom (VerboseKey, Type)]
doms [Dom (VerboseKey, Type)]
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. [a] -> [a] -> [a]
++ [Dom (VerboseKey, Type)
dom]
              Defn
_ -> Telescope
tel
  let d' :: Definition
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 :: QName
defName = QName
q }
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.signature" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"lambda-lifted definition =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Definition -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Definition
d'
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions ((Definitions -> Definitions) -> Signature -> Signature)
-> (Definitions -> Definitions) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Definition -> Definition -> Definition)
-> QName -> Definition -> Definitions -> Definitions
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith Definition -> Definition -> Definition
(+++) QName
q Definition
d'
  MutualId
i <- TCM MutualId
currentOrFreshMutualBlock
  MutualId -> QName -> TCM ()
setMutualBlock MutualId
i QName
q
  where
    Definition
new +++ :: Definition -> Definition -> Definition
+++ Definition
old = Definition
new { defDisplay :: [LocalDisplayForm]
defDisplay = Definition -> [LocalDisplayForm]
defDisplay Definition
new [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. [a] -> [a] -> [a]
++ Definition -> [LocalDisplayForm]
defDisplay Definition
old
                      , defInstance :: Maybe QName
defInstance = Definition -> Maybe QName
defInstance Definition
new Maybe QName -> Maybe QName -> Maybe QName
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Definition -> Maybe QName
defInstance Definition
old }

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

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

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

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

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

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

-- | Lifts clauses to the top-level and adds them to definition.
--   Also adjusts the 'funCopatternLHS' field if necessary.
addClauses :: QName -> [Clause] -> TCM ()
addClauses :: QName -> [Clause] -> TCM ()
addClauses QName
q [Clause]
cls = do
  Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$
    (Defn -> Defn) -> Definition -> Definition
updateTheDef (([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) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
|| [Clause] -> Bool
isCopatternLHS [Clause]
cls)

mkPragma :: String -> TCM CompilerPragma
mkPragma :: VerboseKey -> TCM CompilerPragma
mkPragma VerboseKey
s = Range -> VerboseKey -> CompilerPragma
CompilerPragma (Range -> VerboseKey -> CompilerPragma)
-> TCMT IO Range -> TCMT IO (VerboseKey -> 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 (VerboseKey -> CompilerPragma)
-> TCMT IO VerboseKey -> TCM CompilerPragma
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VerboseKey -> TCMT IO VerboseKey
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerboseKey
s

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

  where

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

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

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

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

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

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

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

-- | Add a section to the signature.
--
--   The current context will be stored as the cumulative module parameters
--   for this section.
addSection :: ModuleName -> TCM ()
addSection :: ModuleName -> TCM ()
addSection ModuleName
m = do
  Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  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 :: * -> *).
(Functor 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".
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.section" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"warning: redundantly adding existing section" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.section" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"with content" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
    else do
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"overwriting existing section" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"of content  " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec'
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"with content" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Section -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
      TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  -- Add the new section.
  ModuleName -> TCM ()
setModuleCheckpoint ModuleName
m
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Lens' Sections Signature -> LensMap Sections Signature
forall i o. Lens' i o -> LensMap i o
over Lens' Sections Signature
sigSections LensMap Sections Signature -> LensMap Sections Signature
forall a b. (a -> b) -> a -> b
$ ModuleName -> Section -> Sections -> Sections
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModuleName
m Section
sec

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

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

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

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

  -- Compute all unfoldings of x by repeatedly calling reduceDefCopy
  [Term]
vs <- QName -> Term -> TCM [Term]
unfoldings QName
x Term
v
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.display.section" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"unfoldings:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v | Term
v <- [Term]
vs ] ]

  -- Turn unfoldings into display forms
  VerboseLevel
npars <- VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
subtract (Definition -> VerboseLevel
projectionArgs Definition
def) (VerboseLevel -> VerboseLevel)
-> TCMT IO VerboseLevel -> TCMT IO VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
  let dfs :: [(QName, DisplayForm)]
dfs = [Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)])
-> [Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)]
forall a b. (a -> b) -> a -> b
$ (Term -> Maybe (QName, DisplayForm))
-> [Term] -> [Maybe (QName, DisplayForm)]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> Term -> Term -> Maybe (QName, DisplayForm)
displayForm VerboseLevel
npars Term
v) [Term]
vs
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.display.section" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"displayForms:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"-->" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> DisplayForm -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DisplayForm
df) | (QName
y, DisplayForm
df) <- [(QName, DisplayForm)]
dfs ] ]

  -- and add them
  ((QName, DisplayForm) -> TCM ())
-> [(QName, DisplayForm)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((QName -> DisplayForm -> TCM ()) -> (QName, DisplayForm) -> TCM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry QName -> DisplayForm -> TCM ()
addDisplayForm) [(QName, DisplayForm)]
dfs
  where

    -- To get display forms for projections we need to unSpine here.
    view :: Term -> ([Arg ArgName], Term)
    view :: Term -> ([Arg VerboseKey], Term)
view = (Term -> Term)
-> ([Arg VerboseKey], Term) -> ([Arg VerboseKey], Term)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Term -> Term
unSpine (([Arg VerboseKey], Term) -> ([Arg VerboseKey], Term))
-> (Term -> ([Arg VerboseKey], Term))
-> Term
-> ([Arg VerboseKey], Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ([Arg VerboseKey], 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 -> Maybe (QName, DisplayForm)
    displayForm :: VerboseLevel -> Term -> Term -> Maybe (QName, DisplayForm)
displayForm VerboseLevel
npars Term
top Term
v =
      case Term -> ([Arg VerboseKey], Term)
view Term
v of
        ([Arg VerboseKey]
xs, Def QName
y Elims
es)   -> (QName
y,)         (DisplayForm -> (QName, DisplayForm))
-> Maybe DisplayForm -> Maybe (QName, DisplayForm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg VerboseKey] -> Elims -> Maybe DisplayForm
mkDisplay [Arg VerboseKey]
xs Elims
es
        ([Arg VerboseKey]
xs, Con ConHead
h ConInfo
i Elims
es) -> (ConHead -> QName
conName ConHead
h,) (DisplayForm -> (QName, DisplayForm))
-> Maybe DisplayForm -> Maybe (QName, DisplayForm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg VerboseKey] -> Elims -> Maybe DisplayForm
mkDisplay [Arg VerboseKey]
xs Elims
es
        ([Arg VerboseKey], Term)
_ -> Maybe (QName, DisplayForm)
forall a. HasCallStack => a
__IMPOSSIBLE__
      where
        mkDisplay :: [Arg VerboseKey] -> Elims -> Maybe DisplayForm
mkDisplay [Arg VerboseKey]
xs Elims
es = DisplayForm -> Maybe DisplayForm
forall a. a -> Maybe a
Just (VerboseLevel -> Elims -> DisplayTerm -> DisplayForm
Display (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
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 -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
args)
          where
            n :: VerboseLevel
n    = [Arg VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg VerboseKey]
xs
            args :: Args
args = (Arg VerboseKey -> VerboseLevel -> Arg Term)
-> [Arg VerboseKey] -> [VerboseLevel] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg VerboseKey
x VerboseLevel
i -> VerboseLevel -> Term
var VerboseLevel
i Term -> Arg VerboseKey -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg VerboseKey
x) [Arg VerboseKey]
xs (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
n)

    -- Unfold a single defCopy.
    unfoldOnce :: Term -> TCM (Reduced () Term)
    unfoldOnce :: Term -> TCM (Reduced () Term)
unfoldOnce Term
v = case Term -> ([Arg VerboseKey], Term)
view Term
v of
      ([Arg VerboseKey]
xs, Def QName
f Elims
es)   -> ((Reduced () Term -> Reduced () Term)
-> TCM (Reduced () Term) -> TCM (Reduced () Term)
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg VerboseKey] -> Term -> Term
unlamView [Arg VerboseKey]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM QName
f Elims
es)
      ([Arg VerboseKey]
xs, Con ConHead
c ConInfo
i Elims
es) -> ((Reduced () Term -> Reduced () Term)
-> TCM (Reduced () Term) -> TCM (Reduced () Term)
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg VerboseKey] -> Term -> Term
unlamView [Arg VerboseKey]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM (ConHead -> QName
conName ConHead
c) Elims
es)
      ([Arg VerboseKey], Term)
_                -> Reduced () Term -> TCM (Reduced () Term)
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      NoReduction{}     -> [Term] -> TCM [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      YesReduction Simplification
_ Term
v' -> do
        let headSymbol :: Maybe QName
headSymbol = case ([Arg VerboseKey], Term) -> Term
forall a b. (a, b) -> b
snd (([Arg VerboseKey], Term) -> Term)
-> ([Arg VerboseKey], Term) -> Term
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg VerboseKey], 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 (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.
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCM Doc
"reduceDefCopy said YesReduction but the head symbol is the same!?"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"v  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"v' =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v'
              ]
            TCM [Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
          Just QName
y -> do
            TCMT IO Bool -> TCM [Term] -> TCM [Term] -> TCM [Term]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Definition -> Bool
defCopy (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
y)
                ((Term
v' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) ([Term] -> [Term]) -> TCM [Term] -> TCM [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Term -> TCM [Term]
unfoldings QName
y Term
v')  -- another copy so keep going
                ([Term] -> TCM [Term]
forall (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 -> Args -> ScopeCopyInfo -> TCM ()
applySection ModuleName
new Telescope
ptel ModuleName
old Args
ts ScopeCopyInfo{ renModules :: ScopeCopyInfo -> Ren ModuleName
renModules = Ren ModuleName
rm, renNames :: ScopeCopyInfo -> Ren QName
renNames = Ren QName
rd } = do
  Ren QName
rd <- Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
rd
  ModuleName
-> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection' ModuleName
new Telescope
ptel ModuleName
old Args
ts ScopeCopyInfo :: Ren ModuleName -> Ren QName -> ScopeCopyInfo
ScopeCopyInfo{ renModules :: Ren ModuleName
renModules = Ren ModuleName
rm, renNames :: Ren QName
renNames = Ren QName
rd }
  where
    -- If a datatype is being copied, all its constructors need to be copied,
    -- and if a constructor is copied its datatype needs to be.
    closeConstructors :: Ren QName -> TCM (Ren QName)
    closeConstructors :: Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
rd = do
        [QName]
ds <- (QName -> QName) -> [QName] -> [QName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn QName -> QName
forall a. a -> a
id ([QName] -> [QName])
-> ([Maybe QName] -> [QName]) -> [Maybe QName] -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [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
<$> (QName -> TCMT IO (Maybe QName))
-> [QName] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCMT IO (Maybe QName)
constructorData (Ren QName -> [QName]
forall k a. Map k a -> [k]
Map.keys Ren QName
rd)
        [QName]
cs <- (QName -> QName) -> [QName] -> [QName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn QName -> QName
forall a. a -> a
id ([QName] -> [QName])
-> ([[QName]] -> [QName]) -> [[QName]] -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[QName]] -> [QName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat    ([[QName]] -> [QName]) -> TCMT IO [[QName]] -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO [QName]) -> [QName] -> TCMT IO [[QName]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCMT IO [QName]
dataConstructors (Ren QName -> [QName]
forall k a. Map k a -> [k]
Map.keys Ren QName
rd)
        Ren QName
new <- (List1 QName -> List1 QName -> List1 QName)
-> [Ren QName] -> Ren QName
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith List1 QName -> List1 QName -> List1 QName
forall a. Semigroup a => a -> a -> a
(<>) ([Ren QName] -> Ren QName)
-> TCMT IO [Ren QName] -> TCM (Ren QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Ren QName)) -> [QName] -> TCMT IO [Ren QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCM (Ren QName)
rename ([QName]
ds [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ [QName]
cs)
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply.complete" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCM Doc
"also copying: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Ren QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Ren QName
new
        Ren QName -> TCM (Ren QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ren QName -> TCM (Ren QName)) -> Ren QName -> TCM (Ren QName)
forall a b. (a -> b) -> a -> b
$ (List1 QName -> List1 QName -> List1 QName)
-> Ren QName -> Ren QName -> Ren QName
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith List1 QName -> List1 QName -> List1 QName
forall a. Semigroup a => a -> a -> a
(<>) Ren QName
new Ren QName
rd
      where
        rename :: QName -> TCM (Ren QName)
        rename :: QName -> TCM (Ren QName)
rename 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 (f :: * -> *) a. Applicative f => a -> f a
pure Ren QName
forall a. Monoid a => a
mempty
          | Bool
otherwise =
              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 (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
. List1 Name -> QName
qnameFromList (List1 Name -> QName) -> (Name -> List1 Name) -> Name -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> List1 Name
forall el coll. Singleton el coll => el -> coll
singleton (Name -> Ren QName) -> TCMT IO Name -> TCM (Ren QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> VerboseKey) -> Name -> VerboseKey
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)

        constructorData :: QName -> TCM (Maybe QName)
        constructorData :: QName -> TCMT IO (Maybe QName)
constructorData QName
x = do
          (Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x) TCMT IO Defn -> (Defn -> Maybe QName) -> TCMT IO (Maybe QName)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
            Constructor{ conData :: Defn -> QName
conData = QName
d } -> QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d
            Defn
_                          -> Maybe QName
forall a. Maybe a
Nothing

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

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

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

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

    copyDef :: Args -> QName -> QName -> TCM ()
    copyDef :: Args -> QName -> QName -> TCM ()
copyDef Args
ts QName
x QName
y = do
      Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
      VerboseLevel
np  <- ModuleName -> TCMT IO VerboseLevel
argsToUse (QName -> ModuleName
qnameModule QName
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.
      [Hiding]
hidings <- (Dom (VerboseKey, Type) -> Hiding)
-> [Dom (VerboseKey, Type)] -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map Dom (VerboseKey, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ([Dom (VerboseKey, Type)] -> [Hiding])
-> (Telescope -> [Dom (VerboseKey, Type)]) -> Telescope -> [Hiding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList (Telescope -> [Hiding]) -> TCMT IO Telescope -> TCMT IO [Hiding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (QName -> ModuleName
qnameModule QName
x)
      let ts' :: Args
ts' = (Hiding -> Arg Term -> Arg Term) -> [Hiding] -> Args -> Args
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 Args
ts
      Telescope
commonTel <- ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
old (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
x)
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"copyDef" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"->" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y
        , TCM Doc
"ts' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
ts' ]
      Args -> VerboseLevel -> Definition -> TCM ()
copyDef' Args
ts' VerboseLevel
np Definition
def
      where
        copyDef' :: Args -> VerboseLevel -> Definition -> TCM ()
copyDef' Args
ts VerboseLevel
np Definition
d = do
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"making new def for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"from" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"with" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
np) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"args" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show (IsAbstract -> VerboseKey) -> IsAbstract -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Definition -> IsAbstract
defAbstract Definition
d)
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCM Doc
"args = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Args -> VerboseKey
forall a. Show a => a -> VerboseKey
show Args
ts')
            , TCM Doc
"old type = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> Type
defType Definition
d) ]
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCM Doc
"new type = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
          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 QName -> (QName -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe QName
inst ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
c -> QName -> QName -> TCM ()
addNamedInstance QName
y QName
c
          -- 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 || size ptel > 0) $ do
-}
          -- BREAKS fail/Issue1643a
          -- -- Andreas, 2015-09-09 Issue 1643:
          -- -- Do not add a display form for a bare module alias.
          -- when (not isCon && size ptel == 0 && not (null ts)) $ do
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ptel VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            QName -> TCM ()
addDisplayForms QName
y
          where
            ts' :: Args
ts' = VerboseLevel -> Args -> Args
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
np Args
ts
            t :: Type
t   = Definition -> Type
defType Definition
d Type -> Args -> Type
`piApply` Args
ts'
            pol :: [Polarity]
pol = Definition -> [Polarity]
defPolarity Definition
d [Polarity] -> Args -> [Polarity]
forall t. Apply t => t -> Args -> t
`apply` Args
ts'
            occ :: [Occurrence]
occ = Definition -> [Occurrence]
defArgOccurrences Definition
d [Occurrence] -> Args -> [Occurrence]
forall t. Apply t => t -> Args -> t
`apply` Args
ts'
            gen :: NumGeneralizableArgs
gen = Definition -> NumGeneralizableArgs
defArgGeneralizable Definition
d NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
`apply` Args
ts'
            inst :: Maybe QName
inst = Definition -> Maybe QName
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.
              Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
              TCMT IO Defn -> (Defn -> Definition) -> TCMT IO Definition
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for TCMT IO Defn
def ((Defn -> Definition) -> TCMT IO Definition)
-> (Defn -> Definition) -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ \ Defn
df -> Defn :: ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn
                    { defArgInfo :: ArgInfo
defArgInfo        = Definition -> ArgInfo
defArgInfo Definition
d
                    , defName :: QName
defName           = QName
y
                    , defType :: Type
defType           = Type
t
                    , defPolarity :: [Polarity]
defPolarity       = [Polarity]
pol
                    , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence]
occ
                    , defArgGeneralizable :: NumGeneralizableArgs
defArgGeneralizable = NumGeneralizableArgs
gen
                    , defGeneralizedParams :: [Maybe Name]
defGeneralizedParams = [] -- This is only needed for type checking data/record defs so no need to copy it.
                    , defDisplay :: [LocalDisplayForm]
defDisplay        = []
                    , defMutual :: MutualId
defMutual         = -MutualId
1   -- TODO: mutual block?
                    , defCompiledRep :: CompiledRepresentation
defCompiledRep    = CompiledRepresentation
noCompiledRep
                    , defInstance :: Maybe QName
defInstance       = Maybe QName
inst
                    , defCopy :: Bool
defCopy           = Bool
True
                    , defMatchable :: Set QName
defMatchable      = Set QName
forall a. Set a
Set.empty
                    , defNoCompilation :: Bool
defNoCompilation  = Definition -> Bool
defNoCompilation Definition
d
                    , defInjective :: Bool
defInjective      = Bool
False
                    , defCopatternLHS :: Bool
defCopatternLHS   = [Clause] -> Bool
isCopatternLHS [Clause
cl]
                    , defBlocked :: Blocked_
defBlocked        = Definition -> Blocked_
defBlocked Definition
d
                    , defLanguage :: Language
defLanguage       =
                      case Definition -> Language
defLanguage Definition
d of
                        -- Note that Cubical Agda code can be imported
                        -- when --erased-cubical is used.
                        l :: Language
l@(Cubical Cubical
CFull) -> Language
l
                        Cubical Cubical
CErased   -> Language
lang
                        Language
WithoutK          -> Language
lang
                        Language
WithK             -> Language
lang
                    , theDef :: Defn
theDef            = Defn
df }
            oldDef :: Defn
oldDef = Definition -> Defn
theDef Definition
d
            isCon :: Bool
isCon  = case Defn
oldDef of { Constructor{} -> Bool
True ; Defn
_ -> Bool
False }
            mutual :: Maybe [QName]
mutual = case Defn
oldDef of { Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
m} -> Maybe [QName]
m              ; Defn
_ -> Maybe [QName]
forall a. Maybe a
Nothing }
            extlam :: Maybe ExtLamInfo
extlam = case Defn
oldDef of { Function{funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
e} -> Maybe ExtLamInfo
e              ; Defn
_ -> Maybe ExtLamInfo
forall a. Maybe a
Nothing }
            with :: Maybe QName
with   = case Defn
oldDef of { Function{funWith :: Defn -> Maybe QName
funWith = Maybe QName
w}   -> QName -> QName
copyName (QName -> QName) -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
w ; Defn
_ -> Maybe QName
forall a. Maybe a
Nothing }
            -- Andreas, 2015-05-11, to fix issue 1413:
            -- Even if we apply the record argument (must be @var 0@), we stay a projection.
            -- This is because we may abstract the record argument later again.
            -- See succeed/ProjectionNotNormalized.agda
            isVar0 :: Arg Term -> Bool
isVar0 Arg Term
t = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t of Var VerboseLevel
0 [] -> Bool
True; Term
_ -> Bool
False
            proj :: Maybe Projection
proj   = case Defn
oldDef of
              Function{funProjection :: Defn -> Maybe Projection
funProjection = Just p :: Projection
p@Projection{projIndex :: Projection -> VerboseLevel
projIndex = VerboseLevel
n}}
                | Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts' VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
n Bool -> Bool -> Bool
|| (Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts' VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
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 (Args -> Maybe (Arg Term)
forall a. [a] -> Maybe a
lastMaybe Args
ts'))
                -> Projection -> Maybe Projection
forall a. a -> Maybe a
Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Projection
p { projIndex :: VerboseLevel
projIndex = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts'
                            , projLams :: ProjLams
projLams  = Projection -> ProjLams
projLams Projection
p ProjLams -> Args -> ProjLams
forall t. Apply t => t -> Args -> t
`apply` Args
ts'
                            , projProper :: Maybe QName
projProper= QName -> QName
copyName (QName -> QName) -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Projection -> Maybe QName
projProper Projection
p
                            }
              Defn
_ -> Maybe Projection
forall a. Maybe a
Nothing
            def :: TCMT IO Defn
def =
              case Defn
oldDef of
                Constructor{ conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
np, conData :: Defn -> QName
conData = QName
d } -> Defn -> TCMT IO Defn
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 :: VerboseLevel
conPars = VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts'
                         , conData :: QName
conData = QName -> QName
copyName QName
d
                         }
                Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> Defn -> TCMT IO Defn
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 :: VerboseLevel
dataPars   = VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts'
                         , dataClause :: Maybe Clause
dataClause = Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
cl
                         , dataCons :: [QName]
dataCons   = (QName -> QName) -> [QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map QName -> QName
copyName [QName]
cs
                         }
                Record{ recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
np, recTel :: Defn -> Telescope
recTel = Telescope
tel } -> Defn -> TCMT IO Defn
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 :: VerboseLevel
recPars    = VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ts'
                         , recClause :: Maybe Clause
recClause  = Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
cl
                         , recTel :: Telescope
recTel     = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
ts'
                         }
                Defn
GeneralizableVar -> Defn -> TCMT IO Defn
forall (m :: * -> *) a. Monad m => a -> m a
return Defn
GeneralizableVar
                Defn
_ -> do
                  (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause
cl] -- Andreas, 2012-10-07 non need for record pattern translation
                  let newDef :: Defn
newDef =
                        Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro  (Defn
oldDef Defn -> Lens' Bool Defn -> Bool
forall o i. o -> Lens' i o -> i
^. Lens' Bool Defn
funMacro) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funStatic (Defn
oldDef Defn -> Lens' Bool Defn -> Bool
forall o i. o -> Lens' i o -> i
^. Lens' Bool Defn
funStatic) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funInline Bool
True (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                        Defn
emptyFunction
                        { funClauses :: [Clause]
funClauses        = [Clause
cl]
                        , funCompiled :: Maybe CompiledClauses
funCompiled       = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc
                        , funSplitTree :: Maybe SplitTree
funSplitTree      = Maybe SplitTree
mst
                        , funMutual :: Maybe [QName]
funMutual         = Maybe [QName]
mutual
                        , funProjection :: Maybe Projection
funProjection     = Maybe Projection
proj
                        , funTerminates :: Maybe Bool
funTerminates     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                        , funExtLam :: Maybe ExtLamInfo
funExtLam         = Maybe ExtLamInfo
extlam
                        , funWith :: Maybe QName
funWith           = Maybe QName
with
                        }
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ (TCM Doc
"new def for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Defn -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
newDef
                  Defn -> TCMT IO Defn
forall (m :: * -> *) a. Monad m => a -> m a
return Defn
newDef

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

    {- Example

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

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

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

    For 1.
      Common prefix is: Top
      totalArgs = |Θ|   (section Top)
      tel       = Θ.Γ.Φ (section Top.A.M)
      ts'       = take totalArgs ts
      Θ₂        = drop totalArgs Θ
      new section C.M
        tel =  Θ₂.Γ.Φ[ts']
    -}
    copySec :: Args -> ModuleName -> ModuleName -> TCM ()
    copySec :: Args -> ModuleName -> ModuleName -> TCM ()
copySec Args
ts ModuleName
x ModuleName
y = do
      VerboseLevel
totalArgs <- ModuleName -> TCMT IO VerboseLevel
argsToUse ModuleName
x
      Telescope
tel       <- ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
x
      let sectionTel :: Telescope
sectionTel =  Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel (Args -> Telescope) -> Args -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Args -> Args
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
totalArgs Args
ts
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Copying section" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"to" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
y
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  ts           = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall a. Monoid a => [a] -> a
mconcat (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
List.intersperse TCM Doc
"; " ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
ts))
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  totalArgs    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
totalArgs)
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  tel          = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text ([VerboseKey] -> VerboseKey
unwords ((Dom (VerboseKey, Type) -> VerboseKey)
-> [Dom (VerboseKey, Type)] -> [VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst ((VerboseKey, Type) -> VerboseKey)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Type))
-> Dom (VerboseKey, Type)
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (VerboseKey, Type)] -> [VerboseKey])
-> [Dom (VerboseKey, Type)] -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel))  -- only names
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  sectionTel   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text ([VerboseKey] -> VerboseKey
unwords ((Dom (VerboseKey, Type) -> VerboseKey)
-> [Dom (VerboseKey, Type)] -> [VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst ((VerboseKey, Type) -> VerboseKey)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Type))
-> Dom (VerboseKey, Type)
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (VerboseKey, Type)] -> [VerboseKey])
-> [Dom (VerboseKey, Type)] -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
ptel)) -- only names
      Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sectionTel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCM ()
addSection ModuleName
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
  LocalDisplayForm
d <- DisplayForm -> TCMT IO LocalDisplayForm
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen DisplayForm
df
  let add :: Signature -> Signature
add = QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
x ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> Definition
def{ defDisplay :: [LocalDisplayForm]
defDisplay = LocalDisplayForm
d LocalDisplayForm -> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. a -> [a] -> [a]
: Definition -> [LocalDisplayForm]
defDisplay Definition
def }
  TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
x)
    {-then-} ((Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature Signature -> Signature
add)
    {-else-} (Lens' DisplayForms TCState
stImportsDisplayForms Lens' DisplayForms TCState
-> (DisplayForms -> DisplayForms) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` ([LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm])
-> QName -> [LocalDisplayForm] -> DisplayForms -> DisplayForms
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. [a] -> [a] -> [a]
(++) QName
x [LocalDisplayForm
d])
  TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (QName -> TCMT IO Bool
hasLoopingDisplayForm QName
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCM Doc
"Cannot add recursive display form for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x

isLocal :: ReadTCState m => QName -> m Bool
isLocal :: 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' Definitions TCState -> m Definitions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR ((Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
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' Definitions Signature
sigDefinitions)

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

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

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

canonicalName :: HasConstInfo m => QName -> m QName
canonicalName :: QName -> m QName
canonicalName QName
x = do
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  case Defn
def of
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c}                                -> QName -> m QName
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 (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 :: QName -> QName -> m (Maybe QName)
sameDef QName
d1 QName
d2 = do
  QName
c1 <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d1
  QName
c2 <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d2
  if (QName
c1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
c2) then Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> m (Maybe QName)) -> Maybe QName -> m (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c1 else Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

-- | Can be called on either a (co)datatype, a record type or a
--   (co)constructor.
whatInduction :: MonadTCM tcm => QName -> tcm Induction
whatInduction :: QName -> tcm Induction
whatInduction QName
c = TCM Induction -> tcm Induction
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Induction -> tcm Induction) -> TCM Induction -> tcm Induction
forall a b. (a -> b) -> a -> b
$ do
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  Maybe QName
mz <- VerboseKey -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinName' VerboseKey
builtinIZero
  Maybe QName
mo <- VerboseKey -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinName' VerboseKey
builtinIOne
  case Defn
def of
    Datatype{}                    -> Induction -> TCM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Record{} | Bool -> Bool
not (Defn -> Bool
recRecursive Defn
def) -> Induction -> TCM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
i    } -> Induction -> TCM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return (Induction -> TCM Induction) -> Induction -> TCM Induction
forall a b. (a -> b) -> a -> b
$ Induction -> Maybe Induction -> Induction
forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
i
    Constructor{ conInd :: Defn -> Induction
conInd = Induction
i }     -> Induction -> TCM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
i
    Defn
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mz Bool -> Bool -> Bool
|| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mo
                                  -> Induction -> TCM Induction
forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Defn
_                             -> TCM Induction
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 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
  Defn
d <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Defn
d of
    Record {}                   -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Constructor { conData :: Defn -> QName
conData = QName
d } -> do
      Defn
di <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ case Defn
di of
        Record {}                  -> Bool
True
        Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> [QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [QName]
cs VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
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.

-- | Standard eliminator for 'SigError'.
sigError :: (String -> a) -> a -> SigError -> a
sigError :: (VerboseKey -> a) -> a -> SigError -> a
sigError VerboseKey -> a
f a
a = \case
  SigUnknown VerboseKey
s -> VerboseKey -> a
f VerboseKey
s
  SigError
SigAbstract  -> a
a

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

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

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

  -- Lifting HasConstInfo through monad transformers:

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

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

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

-- | The computation 'getConstInfo' sometimes tweaks the returned
-- 'Definition', depending on the current 'Language' and the
-- 'Language' of the 'Definition'. This variant of 'getConstInfo' does
-- not perform any tweaks.

getOriginalConstInfo ::
  (ReadTCState m, HasConstInfo m) => QName -> m Definition
getOriginalConstInfo :: QName -> m Definition
getOriginalConstInfo QName
q = do
  Definition
def  <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  Language
lang <- m Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
  case (Language
lang, Definition -> Language
defLanguage Definition
def) of
    (Cubical Cubical
CErased, Cubical Cubical
CFull) ->
      Lens' PragmaOptions TCState
-> (PragmaOptions -> PragmaOptions) -> m Definition -> m Definition
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState
        Lens' PragmaOptions TCState
stPragmaOptions
        (\PragmaOptions
opts -> PragmaOptions
opts { optCubical :: Maybe Cubical
optCubical = Cubical -> Maybe Cubical
forall a. a -> Maybe a
Just Cubical
CFull })
        (QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q)
    (Language, Language)
_ -> Definition -> m Definition
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def

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

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

instance HasConstInfo (TCMT IO) where
  getRewriteRulesFor :: QName -> TCMT IO RewriteRules
getRewriteRulesFor = QName -> TCMT IO RewriteRules
forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor
  getConstInfo' :: QName -> TCMT IO (Either SigError Definition)
getConstInfo' QName
q = do
    TCState
st  <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    TCEnv
env <- TCMT IO TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
    TCState -> TCEnv -> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCEnv m) =>
TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q
  getConstInfo :: QName -> TCMT IO Definition
getConstInfo QName
q = QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO Definition)
-> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> Definition -> TCMT IO Definition
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
      Left (SigUnknown VerboseKey
err) -> VerboseKey -> TCMT IO Definition
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail VerboseKey
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
  :: (HasOptions m, MonadDebug m, MonadTCEnv m)
  => TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo :: TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q = do
    let defs :: Definitions
defs  = TCState
stTCState -> Lens' Definitions TCState -> Definitions
forall o i. o -> Lens' i o -> i
^.((Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
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' Definitions Signature
sigDefinitions)
        idefs :: Definitions
idefs = TCState
stTCState -> Lens' Definitions TCState -> Definitions
forall o i. o -> Lens' i o -> i
^.((Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stImports ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Definitions -> f Definitions) -> Signature -> f Signature)
-> (Definitions -> f Definitions)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Definitions Signature
sigDefinitions)
    case [Maybe Definition] -> [Definition]
forall a. [Maybe a] -> [a]
catMaybes [QName -> Definitions -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
defs, QName -> Definitions -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
idefs] of
        []  -> Either SigError Definition -> m (Either SigError Definition)
forall (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
$ VerboseKey -> SigError
SigUnknown (VerboseKey -> SigError) -> VerboseKey -> SigError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Unbound name: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
showQNameId QName
q
        [Definition
d] -> TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env (Definition -> m (Either SigError Definition))
-> m Definition -> m (Either SigError Definition)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> m Definition
forall (m :: * -> *). HasOptions m => Definition -> m Definition
fixQuantity Definition
d
        [Definition]
ds  -> VerboseKey -> m (Either SigError Definition)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ (VerboseKey -> m (Either SigError Definition))
-> VerboseKey -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Ambiguous name: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q
    where
      mkAbs :: TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env Definition
d
        | QName -> TCEnv -> Bool
treatAbstractly' QName
q' TCEnv
env =
          case Definition -> Maybe Definition
makeAbstract Definition
d of
            Just Definition
d      -> Either SigError Definition -> m (Either SigError Definition)
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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> m (Either SigError Definition))
-> Either SigError Definition -> m (Either SigError Definition)
forall a b. (a -> b) -> a -> b
$ Definition -> Either SigError Definition
forall a b. b -> Either a b
Right Definition
d
        where
          q' :: QName
q' = case Definition -> Defn
theDef Definition
d of
            -- Hack to make abstract constructors work properly. The constructors
            -- live in a module with the same name as the datatype, but for 'abstract'
            -- purposes they're considered to be in the same module as the datatype.
            Constructor{} -> QName -> QName
dropLastModule QName
q
            Defn
_             -> QName
q

          dropLastModule :: QName -> QName
dropLastModule q :: QName
q@QName{ qnameModule :: QName -> ModuleName
qnameModule = ModuleName
m } =
            QName
q{ qnameModule :: ModuleName
qnameModule = [Name] -> ModuleName
mnameFromList ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$
                 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
initWithDefault [Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m
             }

      -- Names defined when --cubical is active are (to a large
      -- degree) treated as erased when --erased-cubical is used.
      fixQuantity :: Definition -> m Definition
fixQuantity Definition
d = do
        Language
current <- m Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
        Definition -> m Definition
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> m Definition) -> Definition -> m Definition
forall a b. (a -> b) -> a -> b
$
          if Definition -> Language
defLanguage Definition
d Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
== Cubical -> Language
Cubical Cubical
CFull Bool -> Bool -> Bool
&&
             Language
current Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
== Cubical -> Language
Cubical Cubical
CErased
          then Quantity -> Definition -> Definition
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity Definition
d
          else 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 (BlockT m)

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

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

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

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

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

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

-- | Sets the 'defArgOccurrences' for the given identifier (which
-- should already exist in the signature).
setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m ()
setArgOccurrences :: 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 :: QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d [Occurrence] -> [Occurrence]
f =
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences [Occurrence] -> [Occurrence]
f

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

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

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

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

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

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

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

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

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

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

-- | Set the mutually recursive identifiers.
setMutual :: QName -> [QName] -> TCM ()
setMutual :: QName -> [QName] -> TCM ()
setMutual QName
d [QName]
m = (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \ Defn
def ->
  case Defn
def of
    Function{} -> Defn
def { funMutual :: Maybe [QName]
funMutual = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
m }
    Datatype{} -> Defn
def {dataMutual :: Maybe [QName]
dataMutual = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
m }
    Record{}   -> Defn
def { recMutual :: Maybe [QName]
recMutual = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([QName] -> Bool)
-> (Maybe [QName] -> [QName]) -> Maybe [QName] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [QName]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [QName] -> Bool) -> TCM (Maybe [QName]) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe [QName])
getMutual QName
d1

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

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

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

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

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

{-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-}
getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m)
                  => ModuleName -> m Nat
getModuleFreeVars :: ModuleName -> m VerboseLevel
getModuleFreeVars ModuleName
m = do
  ModuleName
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
  VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
(+) (VerboseLevel -> VerboseLevel -> VerboseLevel)
-> m VerboseLevel -> m (VerboseLevel -> VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m VerboseLevel
forall (m :: * -> *). MonadTCEnv m => ModuleName -> m VerboseLevel
getAnonymousVariables ModuleName
m m (VerboseLevel -> VerboseLevel)
-> m VerboseLevel -> m VerboseLevel
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size (Telescope -> VerboseLevel) -> m Telescope -> m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m0)

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

  VerboseKey -> VerboseLevel -> TCM Doc -> m Args -> m Args
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"tc.sig.param" VerboseLevel
90 (TCM Doc
"computing module parameters of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m) (m Args -> m Args) -> m Args -> m Args
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 Args -> (Substitution -> m Args) -> m Args
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) (Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return []) ((Substitution -> m Args) -> m Args)
-> (Substitution -> m Args) -> m Args
forall a b. (a -> b) -> a -> b
$ \Substitution
sub -> do

  VerboseKey -> VerboseLevel -> TCM Doc -> m Args -> m Args
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"tc.sig.param" VerboseLevel
60 (do
    [Dom (Name, Type)]
cxt <- TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
    VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"cxt  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> PrettyContext -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Dom (Name, Type)] -> PrettyContext
PrettyContext [Dom (Name, Type)]
cxt)
      , TCM Doc
"sub  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
sub
      ]) (m Args -> m Args) -> m Args -> m Args
forall a b. (a -> b) -> a -> b
$ do

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

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

  ModuleName -> m (Maybe Section)
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m m (Maybe Section) -> (Maybe Section -> m Args) -> m Args
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \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.
      Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return Args
args
    Just (Section Telescope
stel) -> do
      -- The section telescope of @m@ should be as least
      -- as long as the number of free vars @m@ is applied to.
      -- We still check here as in no case, we want @zipWith@ to silently
      -- drop some @args@.
      -- And there are also anonymous modules, thus, the invariant is not trivial.
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
stel VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
args) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return (Args -> m Args) -> Args -> m Args
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Arg Term -> Arg Term)
-> [Dom (VerboseKey, Type)] -> Args -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ !Dom (VerboseKey, Type)
dom (Arg ArgInfo
_ Term
v) -> Term
v Term -> Arg (VerboseKey, Type) -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (VerboseKey, Type) -> Arg (VerboseKey, Type)
forall t a. Dom' t a -> Arg a
argFromDom Dom (VerboseKey, Type)
dom) (Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
stel) Args
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 :: TCM a -> TCM a
inFreshModuleIfFreeParams TCM a
k = do
  Maybe Substitution
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 Maybe Substitution -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Substitution
msub Bool -> Bool -> Bool
|| Maybe Substitution
msub Maybe Substitution -> Maybe Substitution -> Bool
forall a. Eq a => a -> a -> Bool
== Substitution -> Maybe Substitution
forall a. a -> Maybe a
Just Substitution
forall a. Substitution' a
IdS then TCM a
k else do
    ModuleName
m  <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
    ModuleName
m' <- ModuleName -> ModuleName -> ModuleName
qualifyM ModuleName
m (ModuleName -> ModuleName)
-> (Name -> ModuleName) -> Name -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> ModuleName
mnameFromList1 (List1 Name -> ModuleName)
-> (Name -> List1 Name) -> Name -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> List1 Name
forall el coll. Singleton el coll => el -> coll
singleton (Name -> ModuleName) -> TCMT IO Name -> TCMT IO ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            VerboseKey -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (VerboseKey
"_" :: String)
    ModuleName -> TCM ()
addSection ModuleName
m'
    ModuleName -> TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m' TCM a
k

-- | Instantiate a closed definition with the correct part of the current
--   context.
{-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-}
instantiateDef
  :: ( Functor m, HasConstInfo m, HasOptions m
     , ReadTCState m, MonadTCEnv m, MonadDebug m )
  => Definition -> m Definition
instantiateDef :: Definition -> m Definition
instantiateDef Definition
d = do
  Args
vs  <- QName -> m Args
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply (QName -> m Args) -> QName -> m Args
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
d
  VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.sig.inst" VerboseLevel
30 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    [Dom (Name, Type)]
ctx <- m [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
    ModuleName
m   <- m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sig.inst" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"instDef in" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> QName
defName Definition
d) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((Arg Name -> TCM Doc) -> [Arg Name] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Arg Name] -> [TCM Doc]) -> [Arg Name] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Arg Term -> Arg Name) -> [Name] -> Args -> [Arg Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Arg Term -> Arg Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) ([Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Dom (Name, Type) -> Name) -> [Dom (Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) [Dom (Name, Type)]
ctx) Args
vs)
  Definition -> m Definition
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> m Definition) -> Definition -> m Definition
forall a b. (a -> b) -> a -> b
$ Definition
d Definition -> Args -> Definition
forall t. Apply t => t -> Args -> t
`apply` Args
vs

instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
                           ReadTCState m, MonadTCEnv m, MonadDebug m)
                       => RewriteRule -> m RewriteRule
instantiateRewriteRule :: RewriteRule -> m RewriteRule
instantiateRewriteRule RewriteRule
rew = do
  VerboseKey
-> VerboseLevel -> TCM Doc -> m RewriteRule -> m RewriteRule
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting" VerboseLevel
95 (TCM Doc
"instantiating rewrite rule" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (RewriteRule -> QName
rewName RewriteRule
rew) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"to the local context.") (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
forall a b. (a -> b) -> a -> b
$ do
  Args
vs  <- QName -> m Args
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply (QName -> m Args) -> QName -> m Args
forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewName RewriteRule
rew
  let rew' :: RewriteRule
rew' = RewriteRule
rew RewriteRule -> Args -> RewriteRule
forall t. Apply t => t -> Args -> t
`apply` Args
vs
  VerboseKey
-> VerboseLevel -> VerboseKey -> m RewriteRule -> m RewriteRule
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn VerboseKey
"rewriting" VerboseLevel
95 (VerboseKey
"instantiated rewrite rule: ") (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey
-> VerboseLevel -> VerboseKey -> m RewriteRule -> m RewriteRule
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn VerboseKey
"rewriting" VerboseLevel
95 (RewriteRule -> VerboseKey
forall a. Show a => a -> VerboseKey
show RewriteRule
rew') (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
forall a b. (a -> b) -> a -> b
$ do
  RewriteRule -> m RewriteRule
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew'

instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m,
                            ReadTCState m, MonadTCEnv m, MonadDebug m)
                        => RewriteRules -> m RewriteRules
instantiateRewriteRules :: RewriteRules -> m RewriteRules
instantiateRewriteRules = (RewriteRule -> m RewriteRule) -> RewriteRules -> m RewriteRules
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RewriteRule -> m RewriteRule
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRule -> m RewriteRule
instantiateRewriteRule

-- | Give the abstract view of a definition.
makeAbstract :: Definition -> Maybe Definition
makeAbstract :: Definition -> Maybe Definition
makeAbstract Definition
d =
  case Definition -> IsAbstract
defAbstract Definition
d of
    IsAbstract
ConcreteDef -> Definition -> Maybe Definition
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
    IsAbstract
AbstractDef -> do
      Defn
def <- Defn -> Maybe Defn
makeAbs (Defn -> Maybe Defn) -> Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
d
      Definition -> Maybe Definition
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d { defArgOccurrences :: [Occurrence]
defArgOccurrences = [] -- no positivity info for abstract things!
               , defPolarity :: [Polarity]
defPolarity       = [] -- no polarity info for abstract things!
               , theDef :: Defn
theDef = Defn
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 :: m a -> m a
inAbstractMode = (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envAbstractMode :: AbstractMode
envAbstractMode = 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 :: m a -> m a
inConcreteMode = (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envAbstractMode :: AbstractMode
envAbstractMode = AbstractMode
ConcreteMode }

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

-- | Enter concrete or abstract mode depending on whether the given identifier
--   is concrete or abstract.
{-# SPECIALIZE inConcreteOrAbstractMode :: QName -> (Definition -> TCM a) -> TCM a #-}
inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode :: 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.
  Definition
def <- m Definition -> m Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m Definition -> m Definition) -> m Definition -> m Definition
forall a b. (a -> b) -> a -> b
$ QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Definition -> IsAbstract
defAbstract Definition
def of
    IsAbstract
AbstractDef -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Definition -> m a
cont Definition
def
    IsAbstract
ConcreteDef -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Definition -> m a
cont Definition
def

-- | Check whether a name might have to be treated abstractly (either if we're
--   'inAbstractMode' or it's not a local name). Returns true for things not
--   declared abstract as well, but for those 'makeAbstract' will have no effect.
treatAbstractly :: MonadTCEnv m => QName -> m Bool
treatAbstractly :: QName -> m Bool
treatAbstractly QName
q = (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC ((TCEnv -> Bool) -> m Bool) -> (TCEnv -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCEnv -> Bool
treatAbstractly' QName
q

-- | Andreas, 2015-07-01:
--   If the @current@ module is a weak suffix of the identifier module,
--   we can see through its abstract definition if we are abstract.
--   (Then @treatAbstractly'@ returns @False@).
--
--   If I am not mistaken, then we cannot see definitions in the @where@
--   block of an abstract function from the perspective of the function,
--   because then the current module is a strict prefix of the module
--   of the local identifier.
--   This problem is fixed by removing trailing anonymous module name parts
--   (underscores) from both names.
treatAbstractly' :: QName -> TCEnv -> Bool
treatAbstractly' :: QName -> TCEnv -> Bool
treatAbstractly' QName
q TCEnv
env = case TCEnv -> AbstractMode
envAbstractMode TCEnv
env of
  AbstractMode
ConcreteMode       -> Bool
True
  AbstractMode
IgnoreAbstractMode -> Bool
False
  AbstractMode
AbstractMode       -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ModuleName
current ModuleName -> ModuleName -> Bool
`isLeChildModuleOf` ModuleName
m
  where
    current :: ModuleName
current = ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ TCEnv -> ModuleName
envCurrentModule TCEnv
env
    m :: ModuleName
m       = ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
    dropAnon :: ModuleName -> ModuleName
dropAnon (MName [Name]
ms) = [Name] -> ModuleName
MName ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName [Name]
ms

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

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

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

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

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

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

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

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

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

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

-- | Returns @True@ if we are dealing with a proper projection,
--   i.e., not a projection-like function nor a record field value
--   (projection applied to argument).
isProperProjection :: Defn -> Bool
isProperProjection :: Defn -> Bool
isProperProjection Defn
d = Maybe Projection -> Bool -> (Projection -> Bool) -> Bool
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Defn -> Maybe Projection
isProjection_ Defn
d) Bool
False ((Projection -> Bool) -> Bool) -> (Projection -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ Projection
isP ->
  (Projection -> VerboseLevel
projIndex Projection
isP VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
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 -> VerboseLevel
projectionArgs = VerboseLevel
-> (Projection -> VerboseLevel) -> Maybe Projection -> VerboseLevel
forall b a. b -> (a -> b) -> Maybe a -> b
maybe VerboseLevel
0 (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max VerboseLevel
0 (VerboseLevel -> VerboseLevel)
-> (Projection -> VerboseLevel) -> Projection -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
pred (VerboseLevel -> VerboseLevel)
-> (Projection -> VerboseLevel) -> Projection -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Projection -> VerboseLevel
projIndex) (Maybe Projection -> VerboseLevel)
-> (Definition -> Maybe Projection) -> Definition -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe Projection
isRelevantProjection_

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

-- | Apply a function @f@ to its first argument, producing the proper
--   postfix projection if @f@ is a projection which is not irrelevant.
applyDef :: (HasConstInfo m)
         => ProjOrigin -> QName -> Arg Term -> m Term
applyDef :: ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f Arg Term
a = do
  let fallback :: m Term
fallback = Term -> m Term
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' Term
forall a. Arg a -> Elim' a
Apply Arg Term
a]
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  m (Maybe Projection) -> m Term -> (Projection -> m Term) -> m Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) m Term
fallback ((Projection -> m Term) -> m Term)
-> (Projection -> m Term) -> m Term
forall a b. (a -> b) -> a -> b
$ \ Projection
isP -> do
    if Projection -> VerboseLevel
projIndex Projection
isP VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
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 (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' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o (QName -> Elim' Term) -> QName -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Projection -> QName
projOrig Projection
isP]