{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Monad.Signature where

import Prelude hiding (null)

import qualified Control.Monad.Fail as Fail

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

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

import Agda.Interaction.Options

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

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Mutual
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import {-# SOURCE #-} Agda.TypeChecking.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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.signature" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding constant " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" to signature"
  Telescope
tel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let tel' :: Telescope
tel' = forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
"r" forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
d of
              Constructor{} -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. LensHiding a => a -> a
hideOrKeepInstance Telescope
tel
              Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projProper :: Projection -> Maybe QName
projProper = Just{}, projIndex :: Projection -> Int
projIndex = Int
n } } ->
                let fallback :: Telescope
fallback = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. LensHiding a => a -> a
hideOrKeepInstance Telescope
tel in
                if Int
n forall a. Ord a => a -> a -> Bool
> Int
0 then Telescope
fallback else
                -- if the record value is part of the telescope, its hiding should left unchanged
                  case forall a. [a] -> Maybe ([a], a)
initLast forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel of
                    Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
Nothing -> Telescope
fallback
                    Just ([Dom ([Char], Type)]
doms, Dom ([Char], Type)
dom) -> [Dom ([Char], Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. LensHiding a => a -> a
hideOrKeepInstance [Dom ([Char], Type)]
doms forall a. [a] -> [a] -> [a]
++ [Dom ([Char], Type)
dom]
              Defn
_ -> Telescope
tel
  let d' :: Definition
d' = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel' forall a b. (a -> b) -> a -> b
$ Definition
d { defName :: QName
defName = QName
q }
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.signature" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"lambda-lifted definition =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Definition
d'
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions forall a b. (a -> b) -> a -> b
$ 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 forall a. [a] -> [a] -> [a]
++ Definition -> [LocalDisplayForm]
defDisplay Definition
old
                      , defInstance :: Maybe QName
defInstance = Definition -> Maybe QName
defInstance Definition
new 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 <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
  QName -> Definition -> TCM ()
addConstant QName
q 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 :: MonadTCState m => QName -> Bool -> m ()
setTerminates :: forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
setTerminates QName
q Bool
b = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
    def :: Defn
def@Function{} -> Defn
def { funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
b }
    def :: Defn
def@Record{}   -> Defn
def { recTerminates :: Maybe Bool
recTerminates = 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 = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef 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 = 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 = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef 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 = 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 =
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ ([Clause] -> [Clause]) -> Defn -> Defn
updateFunClauses [Clause] -> [Clause]
f

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

  -- Jesper, 2022-10-13: unblock any constraints that were
  -- waiting for more clauses of this function
  forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' forall a b. (a -> b) -> a -> b
$ QName -> Blocker -> WakeUp
wakeIfBlockedOnDef QName
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker

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

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

  where

  erased :: TCM Bool
  erased :: TCM Bool
erased = do
    Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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{} ->
        forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC      Lens' (Maybe [Char]) TCEnv
eActiveBackendName (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
b) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' [Backend] TCState
stBackends         (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ [Backend]
builtinBackends) forall a b. (a -> b) -> a -> b
$
        QName -> TCM Bool
isErasable QName
q
     -- Otherwise (Axiom, Datatype, Record type, etc.) we keep it
      Defn
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma :: [Char] -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma [Char]
backend QName
q = do
  [CompilerPragma]
ps <- [Char] -> Definition -> [CompilerPragma]
defCompilerPragmas [Char]
backend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case [CompilerPragma]
ps of
    []  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    [CompilerPragma
p] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just CompilerPragma
p
    (CompilerPragma
_:CompilerPragma
p1:[CompilerPragma]
_) ->
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange CompilerPragma
p1 forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Conflicting " forall a. [a] -> [a] -> [a]
++ [Char]
backend forall a. [a] -> [a] -> [a]
++ [Char]
" pragmas for") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"at") Int
2 forall a b. (a -> b) -> a -> b
$
                       forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (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 = forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set (Lens' Defn Definition
lensTheDef 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 = forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q 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 = 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 (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Sections
a Sections
a')
          (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)
          (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith 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 <- 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!
  forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m) forall a b. (a -> b) -> a -> b
$ \ Section
sec' -> do
    -- At least not with different content!
    if (Section
sec 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".
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"warning: redundantly adding existing section" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with content" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
    else do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"overwriting existing section" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"of content  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec'
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with content" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Section
sec
      forall a. HasCallStack => a
__IMPOSSIBLE__
  -- Add the new section.
  ModuleName -> TCM ()
setModuleCheckpoint ModuleName
m
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' Sections Signature
sigSections forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` 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 :: forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m = do
  Sections
sig  <- (forall o i. o -> Lens' i o -> i
^. Lens' Signature TCState
stSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Sections Signature
sigSections) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  Sections
isig <- (forall o i. o -> Lens' i o -> i
^. Lens' Signature TCState
stImports   forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Sections Signature
sigSections) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m Sections
sig forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` 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 :: forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Tele a
EmptyTel (forall o i. o -> Lens' i o -> i
^. Lens' Telescope Section
secTelescope) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.display.section" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Computing display forms for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x
  Definition
def <- 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.display.section" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"unfoldings:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v | Term
v <- [Term]
vs ] ]

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

  -- and add them
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (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 [Char]], Term)
view = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Term -> Term
unSpine forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ([Arg [Char]], Term)
lamView

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

    -- Unfold a single defCopy.
    unfoldOnce :: Term -> TCM (Reduced () Term)
    unfoldOnce :: Term -> TCM (Reduced () Term)
unfoldOnce Term
v = case Term -> ([Arg [Char]], Term)
view Term
v of
      ([Arg [Char]]
xs, Def QName
f Elims
es)   -> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM QName
f Elims
es)
      ([Arg [Char]]
xs, Con ConHead
c ConInfo
i Elims
es) -> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ([Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs) (QName -> Elims -> TCM (Reduced () Term)
reduceDefCopyTCM (ConHead -> QName
conName ConHead
c) Elims
es)
      ([Arg [Char]], Term)
_                -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      NoReduction{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return []
      YesReduction Simplification
_ Term
v' -> do
        let headSymbol :: Maybe QName
headSymbol = case forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
view Term
v' of
              Def QName
y Elims
_   -> forall a. a -> Maybe a
Just QName
y
              Con ConHead
y ConInfo
_ Elims
_ -> forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
y)
              Term
_         -> forall a. Maybe a
Nothing
        case Maybe QName
headSymbol of
          Maybe QName
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
          Just QName
y | QName
x 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.
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"reduceDefCopy said YesReduction but the head symbol is the same!?"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v'
              ]
            forall a. HasCallStack => a
__IMPOSSIBLE__
          Just QName
y -> do
            forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Definition -> Bool
defCopy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
y)
                ((Term
v' forall a. a -> [a] -> [a]
:) 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
                (forall (m :: * -> *) a. Monad m => a -> m a
return [Term
v'])                 -- not a copy, we stop

-- | Module application (followed by module parameter abstraction).
applySection
  :: ModuleName     -- ^ Name of new module defined by the module macro.
  -> Telescope      -- ^ Parameters of new module.
  -> ModuleName     -- ^ Name of old module applied to arguments.
  -> Args           -- ^ Arguments of module application.
  -> ScopeCopyInfo  -- ^ Imported names and modules
  -> TCM ()
applySection :: ModuleName
-> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
applySection ModuleName
new Telescope
ptel ModuleName
old [Arg Term]
ts ScopeCopyInfo{ renModules :: ScopeCopyInfo -> Ren ModuleName
renModules = Ren ModuleName
rm, renNames :: ScopeCopyInfo -> Ren QName
renNames = Ren QName
rd } = do
  Ren QName
rd <- Ren QName -> TCM (Ren QName)
closeConstructors Ren QName
rd
  ModuleName
-> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
applySection' ModuleName
new Telescope
ptel ModuleName
old [Arg Term]
ts 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 <- forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCM (Maybe QName)
constructorData (forall k a. Map k a -> [k]
Map.keys Ren QName
rd)
        [QName]
cs <- forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCMT IO [QName]
dataConstructors (forall k a. Map k a -> [k]
Map.keys Ren QName
rd)
        Ren QName
new <- forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. [a] -> [a] -> [a]
++ [QName]
cs)
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply.complete" Int
30 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"also copying: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Ren QName
new
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith 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 forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Ren QName
rd = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
          | Bool
otherwise =
              forall k a. k -> a -> Map k a
Map.singleton QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> QName
qnameFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall el coll. Singleton el coll => el -> coll
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)

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

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

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"applySection"
    , TCMT IO Doc
"new  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
new
    , TCMT IO Doc
"ptel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
ptel
    , TCMT IO Doc
"old  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
old
    , TCMT IO Doc
"ts   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Arg Term]
ts
    ]
  Map QName (NonEmpty ())
_ <- forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg Term] -> QName -> QName -> TCM ()
copyDef [Arg Term]
ts) Ren QName
rd
  Map ModuleName (NonEmpty ())
_ <- forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg Term] -> ModuleName -> ModuleName -> TCM ()
copySec [Arg Term]
ts) Ren ModuleName
rm
  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 (forall k a. Map k a -> [a]
Map.elems Ren QName
rd forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall l. IsList l => l -> [Item l]
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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe QName
x forall a. NonEmpty a -> a
List1.head (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x Ren QName
rd)

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

    copyDef :: Args -> QName -> QName -> TCM ()
    copyDef :: [Arg Term] -> QName -> QName -> TCM ()
copyDef [Arg Term]
ts QName
x QName
y = do
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
      Int
np  <- ModuleName -> TCMT IO Int
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 <- forall a b. (a -> b) -> [a] -> [b]
map forall a. LensHiding a => a -> Hiding
getHiding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (QName -> ModuleName
qnameModule QName
x)
      let ts' :: [Arg Term]
ts' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. LensHiding a => Hiding -> a -> a
setHiding [Hiding]
hidings [Arg Term]
ts
      Telescope
commonTel <- forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
old forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
x)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"copyDef" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y
        , TCMT IO Doc
"ts' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Arg Term]
ts' ]
      [Arg Term] -> Int -> Definition -> TCM ()
copyDef' [Arg Term]
ts' Int
np Definition
def
      where
        copyDef' :: [Arg Term] -> Int -> Definition -> TCM ()
copyDef' [Arg Term]
ts Int
np Definition
d = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"making new def for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
y forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Int
np) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"args" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Definition -> IsAbstract
defAbstract Definition
d)
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"args = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show [Arg Term]
ts')
            , TCMT IO Doc
"old type = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> Type
defType Definition
d) ]
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"new type = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
          QName -> Definition -> TCM ()
addConstant QName
y forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM 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`.
          forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe QName
inst 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Sized a => a -> Int
size Telescope
ptel forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$ do
            QName -> TCM ()
addDisplayForms QName
y
          where
            ts' :: [Arg Term]
ts' = forall a. Int -> [a] -> [a]
take Int
np [Arg Term]
ts
            t :: Type
t   = Definition -> Type
defType Definition
d Type -> [Arg Term] -> Type
`piApply` [Arg Term]
ts'
            pol :: [Polarity]
pol = Definition -> [Polarity]
defPolarity Definition
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
            occ :: [Occurrence]
occ = Definition -> [Occurrence]
defArgOccurrences Definition
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
            gen :: NumGeneralizableArgs
gen = Definition -> NumGeneralizableArgs
defArgGeneralizable Definition
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
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 -> TCM Definition
nd QName
y = do
              -- The arguments may use some feature of the current
              -- language.
              Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
              forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for TCMT IO Defn
def forall a b. (a -> b) -> a -> b
$ \ Defn
df -> Defn
                    { defArgInfo :: ArgInfo
defArgInfo        = Definition -> ArgInfo
defArgInfo Definition
d
                    , defName :: QName
defName           = QName
y
                    , defType :: Type
defType           = Type
t
                    , defPolarity :: [Polarity]
defPolarity       = [Polarity]
pol
                    , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence]
occ
                    , 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      = 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
_ -> 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
_ -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
w ; Defn
_ -> 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 forall e. Arg e -> e
unArg Arg Term
t of Var Int
0 [] -> Bool
True; Term
_ -> Bool
False
            proj :: Either ProjectionLikenessMissing Projection
            proj :: Either ProjectionLikenessMissing Projection
proj   = case Defn
oldDef of
              Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right p :: Projection
p@Projection{projIndex :: Projection -> Int
projIndex = Int
n}}
                | forall a. Sized a => a -> Int
size [Arg Term]
ts' forall a. Ord a => a -> a -> Bool
< Int
n Bool -> Bool -> Bool
|| (forall a. Sized a => a -> Int
size [Arg Term]
ts' forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Arg Term -> Bool
isVar0 (forall a. [a] -> Maybe a
lastMaybe [Arg Term]
ts'))
                -> forall a b. b -> Either a b
Right Projection
p { projIndex :: Int
projIndex = Int
n forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size [Arg Term]
ts'
                           , projLams :: ProjLams
projLams  = Projection -> ProjLams
projLams Projection
p forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts'
                           , projProper :: Maybe QName
projProper= QName -> QName
copyName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Projection -> Maybe QName
projProper Projection
p
                           }
              -- Preserve no-projection-likeness flag if it exists, and
              -- it's set to @Left _@. For future reference: The match
              -- on left can't be simplified or it accidentally
              -- circumvents the guard above.
              Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
projl} -> forall a b. a -> Either a b
Left ProjectionLikenessMissing
projl
              Defn
_ -> forall a b. a -> Either a b
Left ProjectionLikenessMissing
MaybeProjection
            def :: TCMT IO Defn
def =
              case Defn
oldDef of
                Constructor{ conPars :: Defn -> Int
conPars = Int
np, conData :: Defn -> QName
conData = QName
d } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { conPars :: Int
conPars = Int
np forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size [Arg Term]
ts'
                         , conData :: QName
conData = QName -> QName
copyName QName
d
                         }
                Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { dataPars :: Int
dataPars   = Int
np forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size [Arg Term]
ts'
                         , dataClause :: Maybe Clause
dataClause = forall a. a -> Maybe a
Just Clause
cl
                         , dataCons :: [QName]
dataCons   = forall a b. (a -> b) -> [a] -> [b]
map QName -> QName
copyName [QName]
cs
                         }
                Record{ recPars :: Defn -> Int
recPars = Int
np, recTel :: Defn -> Telescope
recTel = Telescope
tel } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                  Defn
oldDef { recPars :: Int
recPars    = Int
np forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size [Arg Term]
ts'
                         , recClause :: Maybe Clause
recClause  = forall a. a -> Maybe a
Just Clause
cl
                         , recTel :: Telescope
recTel     = forall t. Apply t => t -> [Arg Term] -> t
apply Telescope
tel [Arg Term]
ts'
                         }
                Defn
GeneralizableVar -> 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 forall a. Maybe a
Nothing [Clause
cl] -- Andreas, 2012-10-07 non need for record pattern translation
                  let newDef :: Defn
newDef =
                        forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro  (Defn
oldDef forall o i. o -> Lens' i o -> i
^. Lens' Bool Defn
funMacro) forall a b. (a -> b) -> a -> b
$
                        forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funStatic (Defn
oldDef forall o i. o -> Lens' i o -> i
^. Lens' Bool Defn
funStatic) forall a b. (a -> b) -> a -> b
$
                        forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funInline Bool
True forall a b. (a -> b) -> a -> b
$
                        FunctionData -> Defn
FunctionDefn FunctionData
emptyFunctionData
                        { _funClauses :: [Clause]
_funClauses        = [Clause
cl]
                        , _funCompiled :: Maybe CompiledClauses
_funCompiled       = forall a. a -> Maybe a
Just CompiledClauses
cc
                        , _funSplitTree :: Maybe SplitTree
_funSplitTree      = Maybe SplitTree
mst
                        , _funMutual :: Maybe [QName]
_funMutual         = Maybe [QName]
mutual
                        , _funProjection :: Either ProjectionLikenessMissing Projection
_funProjection     = Either ProjectionLikenessMissing Projection
proj
                        , _funTerminates :: Maybe Bool
_funTerminates     = forall a. a -> Maybe a
Just Bool
True
                        , _funExtLam :: Maybe ExtLamInfo
_funExtLam         = Maybe ExtLamInfo
extlam
                        , _funWith :: Maybe QName
_funWith           = Maybe QName
with
                        }
                  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"new def for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
newDef
                  forall (m :: * -> *) a. Monad m => a -> m a
return Defn
newDef

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

    {- Example

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

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

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

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

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

getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
getDisplayForms :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [LocalDisplayForm]
getDisplayForms QName
q = do
  [LocalDisplayForm]
ds  <- forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const []) Definition -> [LocalDisplayForm]
defDisplay forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q
  [LocalDisplayForm]
ds1 <- forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault [] QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' DisplayForms TCState
stImportsDisplayForms
  [LocalDisplayForm]
ds2 <- forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault [] QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' DisplayForms TCState
stImportedDisplayForms
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
q) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [LocalDisplayForm]
ds forall a. [a] -> [a] -> [a]
++ [LocalDisplayForm]
ds1 forall a. [a] -> [a] -> [a]
++ [LocalDisplayForm]
ds2)
                  (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [LocalDisplayForm]
ds1 forall a. [a] -> [a] -> [a]
++ [LocalDisplayForm]
ds 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 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 []       = forall (f :: * -> *) a. Applicative f => a -> f a
pure Set QName
used
    go Set QName
used (QName
q : [QName]
qs) = do
      let rhs :: DisplayForm -> DisplayTerm
rhs (Display Int
_ Elims
_ DisplayTerm
e) = DisplayTerm
e   -- Only look at names in the right-hand side (#1870)
      let notYetUsed :: QName -> Set QName
notYetUsed QName
x = if QName
x forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
used then forall a. Set a
Set.empty else forall a. a -> Set a
Set.singleton QName
x
      Set QName
ds <- forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' QName -> Set QName
notYetUsed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (DisplayForm -> DisplayTerm
rhs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Decoration t => t a -> a
dget)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [LocalDisplayForm]
getDisplayForms QName
q forall a. TCM a -> (TCErr -> TCM a) -> TCM a
`catchError_` \ TCErr
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [])  -- might be a pattern synonym
      Set QName -> [QName] -> TCM (Set QName)
go (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
ds Set QName
used) (forall a. Set a -> [a]
Set.toList Set QName
ds forall a. [a] -> [a] -> [a]
++ [QName]
qs)

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

canonicalName :: HasConstInfo m => QName -> m QName
canonicalName :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
x = do
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  case Defn
def of
    Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c}                                -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 })}    -> 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 })} -> forall {m :: * -> *}. HasConstInfo m => Maybe Term -> m QName
can Maybe Term
body
    Defn
_                                                         -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  where
    can :: Maybe Term -> m QName
can Maybe Term
body = forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName forall a b. (a -> b) -> a -> b
$ Term -> QName
extract forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe Term
body
    extract :: Term -> QName
extract (Def QName
x Elims
_)  = QName
x
    extract Term
_          = forall a. HasCallStack => a
__IMPOSSIBLE__

sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
sameDef :: forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d1 QName
d2 = do
  QName
c1 <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d1
  QName
c2 <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d2
  if (QName
c1 forall a. Eq a => a -> a -> Bool
== QName
c2) then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
c1 else forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Induction
whatInduction QName
c = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  Maybe QName
mz <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinIZero
  Maybe QName
mo <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinIOne
  case Defn
def of
    Datatype{}                    -> forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Record{} | Bool -> Bool
not (Defn -> Bool
recRecursive Defn
def) -> forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
i    } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
i
    Constructor{ conInd :: Defn -> Induction
conInd = Induction
i }     -> forall (m :: * -> *) a. Monad m => a -> m a
return Induction
i
    Defn
_ | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
mz Bool -> Bool -> Bool
|| forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
mo
                                  -> forall (m :: * -> *) a. Monad m => a -> m a
return Induction
Inductive
    Defn
_                             -> 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 -> TCM Bool
singleConstructorType QName
q = do
  Defn
d <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Defn
d of
    Record {}                   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Constructor { conData :: Defn -> QName
conData = QName
d } -> do
      Defn
di <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Defn
di of
        Record {}                  -> Bool
True
        Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== Int
1
        Defn
_                          -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> 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 :: forall a. ([Char] -> a) -> a -> SigError -> a
sigError [Char] -> a
f a
a = \case
  SigUnknown [Char]
s -> [Char] -> a
f [Char]
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 = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
      Left (SigUnknown [Char]
err) -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
err
      Left SigError
SigAbstract      -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$
        [Char]
"Abstract, thus, not in scope: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
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' = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo'

  default getRewriteRulesFor
    :: (HasConstInfo n, MonadTrans t, m ~ t n)
    => QName -> m RewriteRules
  getRewriteRulesFor = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo QName
q = do
  Definition
def  <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
  case (Language
lang, Definition -> Language
defLanguage Definition
def) of
    (Cubical Cubical
CErased, Cubical Cubical
CFull) ->
      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 = forall a. a -> Maybe a
Just Cubical
CFull })
        (forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q)
    (Language, Language)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def

defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules
defaultGetRewriteRulesFor :: forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor QName
q = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
shouldReduceDef QName
q) (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$ do
  TCState
st <- forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  let sig :: Signature
sig = TCState
stforall o i. o -> Lens' i o -> i
^.Lens' Signature TCState
stSignature
      imp :: Signature
imp = TCState
stforall o i. o -> Lens' i o -> i
^.Lens' Signature TCState
stImports
      look :: Signature -> Maybe RewriteRules
look Signature
s = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q forall a b. (a -> b) -> a -> b
$ Signature
s forall o i. o -> Lens' i o -> i
^. Lens' RewriteRuleMap Signature
sigRewriteRules
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ 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 :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
q = Projection -> QName
projOrig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
q

instance HasConstInfo (TCMT IO) where
  getRewriteRulesFor :: QName -> TCMT IO RewriteRules
getRewriteRulesFor = forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor
  getConstInfo' :: QName -> TCMT IO (Either SigError Definition)
getConstInfo' QName
q = do
    TCState
st  <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
    TCEnv
env <- forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
    forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCEnv m) =>
TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q
  getConstInfo :: QName -> TCM Definition
getConstInfo QName
q = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
      Left (SigUnknown [Char]
err) -> forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
err
      Left SigError
SigAbstract      -> forall a. QName -> TCM a
notInScopeError 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 :: forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCEnv m) =>
TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo TCState
st TCEnv
env QName
q = do
    let defs :: Definitions
defs  = TCState
stforall o i. o -> Lens' i o -> i
^.(Lens' Signature TCState
stSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Definitions Signature
sigDefinitions)
        idefs :: Definitions
idefs = TCState
stforall o i. o -> Lens' i o -> i
^.(Lens' Signature TCState
stImports forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Definitions Signature
sigDefinitions)
    case forall a. [Maybe a] -> [a]
catMaybes [forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
defs, forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q Definitions
idefs] of
        []  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char] -> SigError
SigUnknown forall a b. (a -> b) -> a -> b
$ [Char]
"Unbound name: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ QName -> [Char]
showQNameId QName
q
        [Definition
d] -> TCEnv -> Definition -> m (Either SigError Definition)
mkAbs TCEnv
env forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {m :: * -> *}. HasOptions m => Definition -> m Definition
fixQuantity Definition
d
        [Definition]
ds  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous name: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
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      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Definition
d
            Maybe Definition
Nothing     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$
                 forall a. [a] -> [a] -> [a]
initWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ 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 <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          if Definition -> Language
defLanguage Definition
d forall a. Eq a => a -> a -> Bool
== Cubical -> Language
Cubical Cubical
CFull Bool -> Bool -> Bool
&&
             Language
current forall a. Eq a => a -> a -> Bool
== Cubical -> Language
Cubical Cubical
CErased
          then 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 :: forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo = forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName

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

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

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

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

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

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

modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences :: forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d [Occurrence] -> [Occurrence]
f =
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d 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 =
  forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
    fun :: Defn
fun@Function{} -> Defn
fun{ funTreeless :: Maybe Compiled
funTreeless = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TTerm -> Maybe [ArgUsage] -> Compiled
Compiled TTerm
t forall a. Maybe a
Nothing }
    Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
getCompiled QName
q = do
  (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q) 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
_                           -> forall a. Maybe a
Nothing

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

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

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

getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage])
getCompiledArgUse :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q = (Compiled -> Maybe [ArgUsage]
cArgUsage forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \ Defn
def ->
  let !cs' :: [QName]
cs' = [QName]
cs forall a. [a] -> [a] -> [a]
++ Defn -> [QName]
dataCons Defn
def in
  case Defn
def of
    Datatype{} -> Defn
def {dataCons :: [QName]
dataCons = [QName]
cs' }
    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_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_ -> forall a. Maybe a
Nothing

-- | Set the mutually recursive identifiers.
setMutual :: QName -> [QName] -> TCM ()
setMutual :: QName -> [QName] -> TCM ()
setMutual QName
d [QName]
m = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
d forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \ Defn
def ->
  case Defn
def of
    Function{} -> Defn
def { funMutual :: Maybe [QName]
funMutual = forall a. a -> Maybe a
Just [QName]
m }
    Datatype{} -> Defn
def {dataMutual :: Maybe [QName]
dataMutual = forall a. a -> Maybe a
Just [QName]
m }
    Record{}   -> Defn
def { recMutual :: Maybe [QName]
recMutual = forall a. a -> Maybe a
Just [QName]
m }
    Defn
_          -> if forall a. Null a => a -> Bool
null [QName]
m then Defn
def else forall a. HasCallStack => a
__IMPOSSIBLE__ -- nothing to do

-- | Check whether two definitions are mutually recursive.
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive QName
d QName
d1 = (QName
d forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ 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_ = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe [QName]
getMutual_

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

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

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

freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m,
                    ReadTCState m, MonadTCEnv m, MonadDebug m)
                => QName -> m Args
freeVarsToApply :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply QName
q = do
  [Arg Term]
vs <- forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply 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 forall a. Null a => a -> Bool
null [Arg Term]
vs then forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
  Type
t <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let TelV Telescope
tel Type
_ = Int -> Type -> TelV Type
telView'UpTo (forall a. Sized a => a -> Int
size [Arg Term]
vs) Type
t
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
tel forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Arg Term]
vs) forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg Term
arg Dom ([Char], Type)
dom -> forall e. Arg e -> e
unArg Arg Term
arg forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall t a. Dom' t a -> Arg a
argFromDom Dom ([Char], Type)
dom) [Arg Term]
vs forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], 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 :: forall (m :: * -> *).
(Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
ModuleName -> m Int
getModuleFreeVars ModuleName
m = do
  ModuleName
m0   <- ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => ModuleName -> m Int
getAnonymousVariables ModuleName
m forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Sized a => a -> Int
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply ModuleName
m = do

  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.sig.param" Int
90 (TCMT IO Doc
"computing module parameters of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m) 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).
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe Substitution)
getModuleParameterSub ModuleName
m) (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$ \Substitution
sub -> do

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

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

  forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m 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.
      forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
    Just (Section Telescope
stel) -> do
      -- The section telescope of @m@ should be as least
      -- as long as the number of free vars @m@ is applied to.
      -- We still check here as in no case, we want @zipWith@ to silently
      -- drop some @args@.
      -- And there are also anonymous modules, thus, the invariant is not trivial.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Sized a => a -> Int
size Telescope
stel forall a. Ord a => a -> a -> Bool
< forall a. Sized a => a -> Int
size [Arg Term]
args) forall a. HasCallStack => a
__IMPOSSIBLE__
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ !Dom ([Char], Type)
dom (Arg ArgInfo
_ Term
v) -> Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall t a. Dom' t a -> Arg a
argFromDom Dom ([Char], Type)
dom) (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
stel) [Arg Term]
args

-- | Unless all variables in the context are module parameters, create a fresh
--   module to capture the non-module parameters. Used when unquoting to make
--   sure generated definitions work properly.
inFreshModuleIfFreeParams :: TCM a -> TCM a
inFreshModuleIfFreeParams :: forall a. TCM a -> TCM a
inFreshModuleIfFreeParams TCM a
k = do
  Maybe Substitution
msub <- forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe Substitution)
getModuleParameterSub forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  if forall a. Maybe a -> Bool
isNothing Maybe Substitution
msub Bool -> Bool -> Bool
|| Maybe Substitution
msub forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just forall a. Substitution' a
IdS then TCM a
k else do
    ModuleName
m  <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
    ModuleName
m' <- ModuleName -> ModuleName -> ModuleName
qualifyM ModuleName
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> ModuleName
mnameFromList1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall el coll. Singleton el coll => el -> coll
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ([Char]
"_" :: String)
    ModuleName -> TCM ()
addSection ModuleName
m'
    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 :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
d = do
  [Arg Term]
vs  <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
d
  forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.sig.inst" Int
30 forall a b. (a -> b) -> a -> b
$ do
    Context
ctx <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
    ModuleName
m   <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sig.inst" Int
30 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"instDef in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
m forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> QName
defName Definition
d) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
ctx) [Arg Term]
vs)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Definition
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs

instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
                           ReadTCState m, MonadTCEnv m, MonadDebug m)
                       => RewriteRule -> m RewriteRule
instantiateRewriteRule :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRule -> m RewriteRule
instantiateRewriteRule RewriteRule
rew = do
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"rewriting" Int
95 (TCMT IO Doc
"instantiating rewrite rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (RewriteRule -> QName
rewName RewriteRule
rew) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to the local context.") forall a b. (a -> b) -> a -> b
$ do
  [Arg Term]
vs  <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewName RewriteRule
rew
  let rew' :: RewriteRule
rew' = RewriteRule
rew forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"rewriting" Int
95 ([Char]
"instantiated rewrite rule: ") forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"rewriting" Int
95 (forall a. Show a => a -> [Char]
show RewriteRule
rew') forall a b. (a -> b) -> a -> b
$ do
  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 :: forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
RewriteRules -> m RewriteRules
instantiateRewriteRules = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Definition
d
    IsAbstract
AbstractDef -> do
      Defn
def <- Defn -> Maybe Defn
makeAbs forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
d
      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{}            = forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@DataOrRecSig{}     = forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@GeneralizableVar{} = forall a. a -> Maybe a
Just Defn
d
    makeAbs d :: Defn
d@Datatype {} = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs d :: Defn
d@Function {} = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs Constructor{} = 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{}    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Defn -> Defn
AbstractDefn Defn
d
    makeAbs Primitive{}   = forall a. HasCallStack => a
__IMPOSSIBLE__
    makeAbs PrimitiveSort{} = forall a. HasCallStack => a
__IMPOSSIBLE__
    makeAbs AbstractDefn{}= forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Enter abstract mode. Abstract definition in the current module are transparent.
{-# SPECIALIZE inAbstractMode :: TCM a -> TCM a #-}
inAbstractMode :: MonadTCEnv m => m a -> m a
inAbstractMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC 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 :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC 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 :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC 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 :: forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q Definition -> m a
cont = do
  -- Andreas, 2015-07-01: If we do not ignoreAbstractMode here,
  -- we will get ConcreteDef for abstract things, as they are turned into axioms.
  Definition
def <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Definition -> IsAbstract
defAbstract Definition
def of
    IsAbstract
AbstractDef -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode forall a b. (a -> b) -> a -> b
$ Definition -> m a
cont Definition
def
    IsAbstract
ConcreteDef -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode 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 :: forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
treatAbstractly QName
q = forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC 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 forall a b. (a -> b) -> a -> b
$ ModuleName
current ModuleName -> ModuleName -> Bool
`isLeChildModuleOf` ModuleName
m
  where
    current :: ModuleName
current = ModuleName -> ModuleName
dropAnon forall a b. (a -> b) -> a -> b
$ TCEnv -> ModuleName
envCurrentModule TCEnv
env
    m :: ModuleName
m       = ModuleName -> ModuleName
dropAnon forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
    dropAnon :: ModuleName -> ModuleName
dropAnon (MName [Name]
ms) = [Name] -> ModuleName
MName forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd 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 :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
q = Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q)

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

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

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

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

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

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

isRelevantProjection_ :: Definition -> Maybe Projection
isRelevantProjection_ :: Definition -> Maybe Projection
isRelevantProjection_ Definition
def =
  if forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
def then forall a. Maybe a
Nothing else Defn -> Maybe Projection
isProjection_ 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 = (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 = (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 = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Defn -> Maybe Projection
isProjection_ Defn
d) Bool
False forall a b. (a -> b) -> a -> b
$ \ Projection
isP ->
  (Projection -> Int
projIndex Projection
isP forall a. Ord a => a -> a -> Bool
> Int
0) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust (Projection -> Maybe QName
projProper Projection
isP)

-- | Number of dropped initial arguments of a projection(-like) function.
projectionArgs :: Definition -> Int
projectionArgs :: Definition -> Int
projectionArgs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 (forall a. Ord a => a -> a -> a
max Int
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> a
pred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Projection -> Int
projIndex) 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 :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
q = Definition -> Bool
defCopatternLHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

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