{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Decl where

import Prelude hiding ( null )

import Control.Monad
import Control.Monad.Writer (tell)

import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Maybe
import qualified Data.Set as Set
import Data.Set (Set)

import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Options

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (deepUnscopeDecl, deepUnscopeDecls)
import Agda.Syntax.Internal
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base ( KindOfName(..) )

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Benchmark (MonadBench, Phase)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level.Solve
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Records
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

import Agda.TypeChecking.Rules.Application
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.Data    ( checkDataDef )
import Agda.TypeChecking.Rules.Record  ( checkRecDef )
import Agda.TypeChecking.Rules.Def     ( checkFunDef, newSection, useTerPragma )
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Display ( checkDisplayPragma )

import Agda.Termination.TermCheck

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Update
import qualified Agda.Utils.SmallSet as SmallSet

import Agda.Utils.Impossible

-- | Cached checkDecl
checkDeclCached :: A.Declaration -> TCM ()
checkDeclCached :: Declaration -> TCM ()
checkDeclCached d :: Declaration
d@A.ScopedDecl{} = Declaration -> TCM ()
checkDecl Declaration
d
checkDeclCached d :: Declaration
d@(A.Section Range
_ ModuleName
mname (A.GeneralizeTel Map QName Name
_ Telescope
tbinds) [Declaration]
_) = do
  Maybe (TypeCheckAction, PostScopeState)
e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog  -- Can ignore the set of generalizable vars (they occur in the telescope)
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache.decl" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDeclCached: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Bool -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Maybe (TypeCheckAction, PostScopeState) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (TypeCheckAction, PostScopeState)
e)
  case Maybe (TypeCheckAction, PostScopeState)
e of
    Just (EnterSection ModuleName
mname' Telescope
tbinds', PostScopeState
_)
      | ModuleName
mname ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
mname' Bool -> Bool -> Bool
&& Telescope
tbinds Telescope -> Telescope -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope
tbinds' -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  TypeCheckAction -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> Telescope -> TypeCheckAction
EnterSection ModuleName
mname Telescope
tbinds
  Declaration -> TCM ()
checkDecl Declaration
d
  TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog TCMT IO (Maybe (TypeCheckAction, PostScopeState))
-> (Maybe (TypeCheckAction, PostScopeState) -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (LeaveSection ModuleName
mname', PostScopeState
_) | ModuleName
mname ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
mname' -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  TypeCheckAction -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> TypeCheckAction
LeaveSection ModuleName
mname

checkDeclCached Declaration
d = do
    Maybe (TypeCheckAction, PostScopeState)
e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog

    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache.decl" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDeclCached: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Bool -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Maybe (TypeCheckAction, PostScopeState) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (TypeCheckAction, PostScopeState)
e)

    case Maybe (TypeCheckAction, PostScopeState)
e of
      (Just (Decl Declaration
d',PostScopeState
s)) | Declaration -> Declaration -> Bool
compareDecl Declaration
d Declaration
d' -> do
        PostScopeState -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m) =>
PostScopeState -> m ()
restorePostScopeState PostScopeState
s
        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache.decl" VerboseLevel
50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"range: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Range -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d)
        Range -> TCM ()
printSyntaxInfo (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d)
      Maybe (TypeCheckAction, PostScopeState)
_ -> do
        TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
        Declaration -> TCM ()
checkDeclWrap Declaration
d
    TypeCheckAction -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TypeCheckAction
Decl Declaration
d
 where
   compareDecl :: Declaration -> Declaration -> Bool
compareDecl A.Section{} A.Section{} = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
   compareDecl A.ScopedDecl{} A.ScopedDecl{} = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
   compareDecl Declaration
x Declaration
y = Declaration
x Declaration -> Declaration -> Bool
forall a. Eq a => a -> a -> Bool
== Declaration
y
   -- changes to CS inside a RecDef or Mutual ought not happen,
   -- but they do happen, so we discard them.
   ignoreChanges :: m a -> m a
ignoreChanges m a
m = m a -> m a
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
     m ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
     m a
m
   checkDeclWrap :: Declaration -> TCM ()
checkDeclWrap d :: Declaration
d@A.RecDef{} = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkDecl Declaration
d
   checkDeclWrap d :: Declaration
d@A.Mutual{} = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkDecl Declaration
d
   checkDeclWrap Declaration
d            = Declaration -> TCM ()
checkDecl Declaration
d

-- | Type check a sequence of declarations.
checkDecls :: [A.Declaration] -> TCM ()
checkDecls :: [Declaration] -> TCM ()
checkDecls [Declaration]
ds = do
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
45 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Checking " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Declaration] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Declaration]
ds) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" declarations..."
  (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDecl [Declaration]
ds

-- | Type check a single declaration.

checkDecl :: A.Declaration -> TCM ()
checkDecl :: Declaration -> TCM ()
checkDecl Declaration
d = Declaration -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Declaration
d (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checking declaration"
    Declaration -> TCM ()
debugPrintDecl Declaration
d
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
90 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> ([Declaration] -> VerboseKey) -> [Declaration] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Declaration] -> VerboseKey
forall a. Show a => a -> VerboseKey
show) (Declaration -> [Declaration]
deepUnscopeDecl Declaration
d)
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Declaration
d  -- Might loop, see e.g. Issue 1597

    let -- What kind of final checks/computations should be performed
        -- if we're not inside a mutual block?
        none :: f a -> f (Maybe a)
none        f a
m = f a
m f a -> Maybe a -> f (Maybe a)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  Maybe a
forall a. Maybe a
Nothing           -- skip all checks
        meta :: f a -> f (Maybe (m ()))
meta        f a
m = f a
m f a -> Maybe (m ()) -> f (Maybe (m ()))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  m () -> Maybe (m ())
forall a. a -> Maybe a
Just (() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())  -- do the usual checks
        mutual :: MutualInfo
-> [Declaration]
-> TCMT IO (MutualId, Set QName)
-> TCMT IO (Maybe (TCM ()))
mutual MutualInfo
i [Declaration]
ds TCMT IO (MutualId, Set QName)
m = TCMT IO (MutualId, Set QName)
m TCMT IO (MutualId, Set QName)
-> ((MutualId, Set QName) -> Maybe (TCM ()))
-> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> TCM () -> Maybe (TCM ())
forall a. a -> Maybe a
Just (TCM () -> Maybe (TCM ()))
-> ((MutualId, Set QName) -> TCM ())
-> (MutualId, Set QName)
-> Maybe (TCM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MutualId -> Set QName -> TCM ())
-> (MutualId, Set QName) -> TCM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (MutualInfo
-> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
mutualChecks MutualInfo
i Declaration
d [Declaration]
ds)
        impossible :: f a -> f b
impossible  f a
m = f a
m f a -> b -> f b
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  b
forall a. HasCallStack => a
__IMPOSSIBLE__
                        -- We're definitely inside a mutual block.

    (Maybe (TCM ())
finalChecks, MetaStore
metas) <- TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore)
forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore))
-> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore)
forall a b. (a -> b) -> a -> b
$ case Declaration
d of
      A.Axiom{}                -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkTypeSignature Declaration
d
      A.Generalize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
checkGeneralize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e
      A.Field{}                -> TypeError -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
FieldOutsideRecord
      A.Primitive DefInfo
i QName
x Arg Expr
e        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ DefInfo -> QName -> Arg Expr -> TCM ()
checkPrimitive DefInfo
i QName
x Arg Expr
e
      A.Mutual MutualInfo
i [Declaration]
ds            -> MutualInfo
-> [Declaration]
-> TCMT IO (MutualId, Set QName)
-> TCMT IO (Maybe (TCM ()))
mutual MutualInfo
i [Declaration]
ds (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ MutualInfo -> [Declaration] -> TCMT IO (MutualId, Set QName)
checkMutual MutualInfo
i [Declaration]
ds
      A.Section Range
_r ModuleName
x GeneralizeTelescope
tel [Declaration]
ds    -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
checkSection ModuleName
x GeneralizeTelescope
tel [Declaration]
ds
      A.Apply ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
ci ImportDirective
_adir -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
ci
      A.Import ModuleInfo
i ModuleName
x ImportDirective
_adir       -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> ModuleName -> TCM ()
checkImport ModuleInfo
i ModuleName
x
      A.Pragma Range
i Pragma
p             -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ Range -> Pragma -> TCM ()
checkPragma Range
i Pragma
p
      A.ScopedDecl ScopeInfo
scope [Declaration]
ds    -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> TCM ()
setScope ScopeInfo
scope TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds
      A.FunDef DefInfo
i QName
x Delayed
delayed [Clause]
cs  -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName -> DefInfo -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
 BenchPhase m ~ Phase, AnyIsAbstract i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef Delayed
delayed DefInfo
i QName
x [Clause]
cs
      A.DataDef DefInfo
i QName
x UniverseCheck
uc DataDefParams
ps [Declaration]
cs   -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName -> DefInfo -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
 BenchPhase m ~ Phase, AnyIsAbstract i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> TCM ()
checkDataDef DefInfo
i QName
x UniverseCheck
uc DataDefParams
ps [Declaration]
cs
      A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs -> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> f b
impossible (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName
-> DefInfo
-> TCMT IO (MutualId, Set QName)
-> TCMT IO (MutualId, Set QName)
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
 BenchPhase m ~ Phase, AnyIsAbstract i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
forall a b. (a -> b) -> a -> b
$ do
                                    DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> TCM ()
checkRecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs
                                    MutualId
blockId <- QName -> TCM MutualId
mutualBlockOf QName
x

                                    -- Andreas, 2016-10-01 testing whether
                                    -- envMutualBlock is set correctly.
                                    -- Apparently not.
                                    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.decl.mutual" VerboseLevel
70 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                                      Maybe MutualId
current <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
                                      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MutualId -> Maybe MutualId
forall a. a -> Maybe a
Just MutualId
blockId Maybe MutualId -> Maybe MutualId -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe MutualId
current) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                                        VerboseKey -> VerboseLevel -> [VerboseKey] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"" VerboseLevel
0
                                          [ VerboseKey
"mutual block id discrepancy for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x
                                          , VerboseKey
"  current    mut. bl. = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe MutualId -> VerboseKey
forall a. Show a => a -> VerboseKey
show Maybe MutualId
current
                                          , VerboseKey
"  calculated mut. bl. = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MutualId -> VerboseKey
forall a. Show a => a -> VerboseKey
show MutualId
blockId
                                          ]

                                    (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MutualId
blockId, QName -> Set QName
forall a. a -> Set a
Set.singleton QName
x)
      A.DataSig DefInfo
i QName
x GeneralizeTelescope
ps Expr
t       -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
DataName DefInfo
i QName
x GeneralizeTelescope
ps Expr
t
      A.RecSig DefInfo
i QName
x GeneralizeTelescope
ps Expr
t        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
RecName DefInfo
i QName
x GeneralizeTelescope
ps Expr
t
                                  -- A record signature is always followed by a
                                  -- record definition. Metas should not be
                                  -- frozen until after the definition has been
                                  -- checked. NOTE: Metas are not frozen
                                  -- immediately after the last field. Perhaps
                                  -- they should be (unless we're in a mutual
                                  -- block).
      A.Open{}                 -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      A.PatternSynDef{}        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a a. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                  -- Open and PatternSynDef are just artifacts
                                  -- from the concrete syntax, retained for
                                  -- highlighting purposes.
      -- Andreas, 2019-08-19, issue #4010, observe @abstract@ also for unquoting.
      -- TODO: is it possible that some of the unquoted declarations/definitions
      -- are abstract and some are not?  Then allowing all to look into abstract things,
      -- as we do here, will leak information about the implementation of abstract things.
      -- TODO: Benchmarking for unquote.
      A.UnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e -> [DefInfo] -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ MutualInfo
-> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
checkUnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e
      A.UnquoteDef [DefInfo]
is [QName]
xs Expr
e     -> TCM () -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ [DefInfo] -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [DefInfo] -> [QName] -> Expr -> TCM ()
checkUnquoteDef [DefInfo]
is [QName]
xs Expr
e

    TCMT IO (Maybe MutualId) -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

      -- Syntax highlighting.
      HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
DontHightlightModuleContents Declaration
d

      -- Defaulting of levels (only when --cumulativity)
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaStore -> TCM ()
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaStore -> m ()
defaultLevelsToZero MetaStore
metas

      -- Post-typing checks.
      Maybe (TCM ()) -> (TCM () -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (TCM ())
finalChecks ((TCM () -> TCM ()) -> TCM ()) -> (TCM () -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ TCM ()
theMutualChecks -> do
        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Attempting to solve constraints before freezing."
        TCM ()
wakeupConstraints_   -- solve emptiness and instance constraints
        Bool
checkingWhere <- (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckingWhere
        DefaultToInfty -> TCM ()
solveSizeConstraints (DefaultToInfty -> TCM ()) -> DefaultToInfty -> TCM ()
forall a b. (a -> b) -> a -> b
$ if Bool
checkingWhere then DefaultToInfty
DontDefaultToInfty else DefaultToInfty
DefaultToInfty
        TCM ()
wakeupConstraints_   -- Size solver might have unblocked some constraints
        case Declaration
d of
            A.Generalize{} -> () -> TCM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Declaration
_ -> do
              VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Freezing all metas."
              TCMT IO IntSet -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO IntSet -> TCM ()) -> TCMT IO IntSet -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaStore -> TCMT IO IntSet
freezeMetas MetaStore
metas

        TCM ()
theMutualChecks

    where

    -- check record or data type signature
    checkSig :: KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
kind DefInfo
i QName
x GeneralizeTelescope
gtel Expr
t = Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' (GeneralizeTelescope -> Maybe GeneralizeTelescope
forall a. a -> Maybe a
Just GeneralizeTelescope
gtel) (Declaration -> TCM ()) -> Declaration -> TCM ()
forall a b. (a -> b) -> a -> b
$
      KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
kind DefInfo
i ArgInfo
defaultArgInfo Maybe [Occurrence]
forall a. Maybe a
Nothing QName
x Expr
t

    -- Switch maybe to abstract mode, benchmark, and debug print bracket.
    check :: forall m i a
          . ( MonadTCEnv m, MonadPretty m, MonadDebug m
            , MonadBench m, Bench.BenchPhase m ~ Phase
            , AnyIsAbstract i )
          => QName -> i -> m a -> m a
    check :: QName -> i -> m a -> m a
check QName
x i
i m a
m = Account (BenchPhase m) -> m a -> m a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
5 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ (TCM Doc
"Checking" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
"."
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl.abstract" VerboseLevel
25 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show (IsAbstract -> VerboseKey) -> IsAbstract -> VerboseKey
forall a b. (a -> b) -> a -> b
$ i -> IsAbstract
forall a. AnyIsAbstract a => a -> IsAbstract
anyIsAbstract i
i
      a
r <- i -> m a -> m a
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly i
i m a
m
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
5 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ (TCM Doc
"Checked" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
"."
      a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

    -- Switch to AbstractMode if any of the i is AbstractDef.
    checkMaybeAbstractly :: forall m i a . ( MonadTCEnv m , AnyIsAbstract i )
                         => i -> m a -> m a
    checkMaybeAbstractly :: i -> m a -> m a
checkMaybeAbstractly = (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a)
-> (i -> TCEnv -> TCEnv) -> i -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' IsAbstract TCEnv -> LensSet IsAbstract TCEnv
forall i o. Lens' i o -> LensSet i o
set forall a. LensIsAbstract a => Lens' IsAbstract a
Lens' IsAbstract TCEnv
lensIsAbstract LensSet IsAbstract TCEnv
-> (i -> IsAbstract) -> i -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> IsAbstract
forall a. AnyIsAbstract a => a -> IsAbstract
anyIsAbstract

-- Some checks that should be run at the end of a mutual block. The
-- set names contains the names defined in the mutual block.
mutualChecks :: Info.MutualInfo -> A.Declaration -> [A.Declaration] -> MutualId -> Set QName -> TCM ()
mutualChecks :: MutualInfo
-> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
mutualChecks MutualInfo
mi Declaration
d [Declaration]
ds MutualId
mid Set QName
names = do
  -- Andreas, 2014-04-11: instantiate metas in definition types
  let nameList :: [QName]
nameList = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names
  (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
instantiateDefinitionType [QName]
nameList
  -- Andreas, 2017-03-23: check positivity before termination.
  -- This allows us to reuse the information about SCCs
  -- to skip termination of non-recursive functions.
  (AllowedReductions -> AllowedReductions) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions (AllowedReduction -> AllowedReductions -> AllowedReductions
forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
SmallSet.delete AllowedReduction
UnconfirmedReductions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    MutualInfo -> Set QName -> TCM ()
checkPositivity_ MutualInfo
mi Set QName
names
  -- Andreas, 2013-02-27: check termination before injectivity,
  -- to avoid making the injectivity checker loop.
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = MutualId -> Maybe MutualId
forall a. a -> Maybe a
Just MutualId
mid }) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Declaration -> TCM ()
checkTermination_ Declaration
d
  [QName] -> TCM ()
revisitRecordPatternTranslation [QName]
nameList -- Andreas, 2016-11-19 issue #2308

  (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
checkIApplyConfluence_ [QName]
nameList

  -- Andreas, 2015-03-26 Issue 1470:
  -- Restricting coinduction to recursive does not solve the
  -- actual problem, and prevents interesting sound applications
  -- of sized types.
  -- checkCoinductiveRecords  ds

  -- Andreas, 2019-07-11: The following remarks about injectivity
  -- and polarity seem outdated, since the UnusedArg Relevance has
  -- been removed.
  -- -- Andreas, 2012-09-11:  Injectivity check stores clauses
  -- -- whose 'Relevance' is affected by polarity computation,
  -- -- so do it here (again).
  -- -- Andreas, 2015-07-01:  In particular, 'UnusedArg's of local functions
  -- -- are only recognized after the polarity computation.
  -- -- See Issue 1366 for an example where injectivity of a local function
  -- -- is used to solve metas.  It fails if we do injectivity analysis
  -- -- before polarity only.
  -- However, we need to repeat injectivity checking after termination checking,
  -- since more reductions are available after termination checking, thus,
  -- more instances of injectivity can be recognized.
  Set QName -> TCM ()
checkInjectivity_        Set QName
names
  Set QName -> TCM ()
checkProjectionLikeness_ Set QName
names

-- | Check if there is a inferred eta record type in the mutual block.
--   If yes, repeat the record pattern translation for all function definitions
--   in the block.
--   This is necessary since the original record pattern translation will
--   have skipped record patterns of the new record types (as eta was off for them).
--   See issue #2308 (and #2197).
revisitRecordPatternTranslation :: [QName] -> TCM ()
revisitRecordPatternTranslation :: [QName] -> TCM ()
revisitRecordPatternTranslation [QName]
qs = do
  -- rs: inferred eta record types of this mutual block
  -- qccs: compiled clauses of definitions
  ([QName]
rs, [(QName, CompiledClauses)]
qccs) <- [Either QName (QName, CompiledClauses)]
-> ([QName], [(QName, CompiledClauses)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either QName (QName, CompiledClauses)]
 -> ([QName], [(QName, CompiledClauses)]))
-> ([Maybe (Either QName (QName, CompiledClauses))]
    -> [Either QName (QName, CompiledClauses)])
-> [Maybe (Either QName (QName, CompiledClauses))]
-> ([QName], [(QName, CompiledClauses)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Either QName (QName, CompiledClauses))]
-> [Either QName (QName, CompiledClauses)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Either QName (QName, CompiledClauses))]
 -> ([QName], [(QName, CompiledClauses)]))
-> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
-> TCMT IO ([QName], [(QName, CompiledClauses)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses))))
-> [QName]
-> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (Either QName (QName, CompiledClauses)))
classify [QName]
qs
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
rs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [(QName, CompiledClauses)]
-> ((QName, CompiledClauses) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(QName, CompiledClauses)]
qccs (((QName, CompiledClauses) -> TCM ()) -> TCM ())
-> ((QName, CompiledClauses) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \(QName
q,CompiledClauses
cc) -> do
    (CompiledClauses
cc, Bool
recordExpressionBecameCopatternLHS) <- ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT (TCMT IO) CompiledClauses
 -> TCMT IO (CompiledClauses, Bool))
-> ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateCompiledClauses ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn)
-> (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Maybe CompiledClauses
-> Maybe CompiledClauses -> Maybe CompiledClauses
forall a b. a -> b -> a
const (Maybe CompiledClauses
 -> Maybe CompiledClauses -> Maybe CompiledClauses)
-> Maybe CompiledClauses
-> Maybe CompiledClauses
-> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc)
      (Definition -> Definition)
-> (Definition -> Definition) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
|| Bool
recordExpressionBecameCopatternLHS)
  where
  -- Walk through the definitions and return the set of inferred eta record types
  -- and the set of function definitions in the mutual block
  classify :: QName -> m (Maybe (Either QName (QName, CompiledClauses)))
classify QName
q = QName
-> (Definition
    -> m (Maybe (Either QName (QName, CompiledClauses))))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> m (Maybe (Either QName (QName, CompiledClauses))))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> (Definition
    -> m (Maybe (Either QName (QName, CompiledClauses))))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
    case Definition -> Defn
theDef Definition
def of
      Record{ recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = Inferred HasEta' PatternOrCopattern
YesEta } -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Either QName (QName, CompiledClauses))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a. a -> Maybe a
Just (Either QName (QName, CompiledClauses)
 -> Maybe (Either QName (QName, CompiledClauses)))
-> Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a b. (a -> b) -> a -> b
$ QName -> Either QName (QName, CompiledClauses)
forall a b. a -> Either a b
Left QName
q
      Function
        { funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
Nothing
            -- Andreas, 2017-08-10, issue #2664:
            -- Do not record pattern translate record projection definitions!
        , funCompiled :: Defn -> Maybe CompiledClauses
funCompiled   = Just CompiledClauses
cc
        } -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Either QName (QName, CompiledClauses))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a. a -> Maybe a
Just (Either QName (QName, CompiledClauses)
 -> Maybe (Either QName (QName, CompiledClauses)))
-> Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a b. (a -> b) -> a -> b
$ (QName, CompiledClauses) -> Either QName (QName, CompiledClauses)
forall a b. b -> Either a b
Right (QName
q, CompiledClauses
cc)
      Defn
_ -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Either QName (QName, CompiledClauses))
forall a. Maybe a
Nothing

type FinalChecks = Maybe (TCM ())

checkUnquoteDecl :: Info.MutualInfo -> [A.DefInfo] -> [QName] -> A.Expr -> TCM FinalChecks
checkUnquoteDecl :: MutualInfo
-> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
checkUnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.unquote.decl" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking unquoteDecl" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
xs)
  Maybe (TCM ())
forall a. Maybe a
Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e

checkUnquoteDef :: [A.DefInfo] -> [QName] -> A.Expr -> TCM ()
checkUnquoteDef :: [DefInfo] -> [QName] -> Expr -> TCM ()
checkUnquoteDef [DefInfo]
_ [QName]
xs Expr
e = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.unquote.decl" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking unquoteDef" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
xs)
  () () -> TCMT IO [QName] -> TCM ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e

-- | Run a reflected TCM computatation expected to define a given list of
--   names.
unquoteTop :: [QName] -> A.Expr -> TCM [QName]
unquoteTop :: [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e = do
  Term
tcm   <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM
  Term
unit  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit
  Term
lzero <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero
  let vArg :: a -> Arg a
vArg = a -> Arg a
forall a. a -> Arg a
defaultArg
      hArg :: a -> Arg a
hArg = Hiding -> Arg a -> Arg a
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg a -> Arg a) -> (a -> Arg a) -> a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Arg a
forall a. a -> Arg a
vArg
  Term
m    <- Quantity -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
zeroQuantity (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
            Expr -> Type -> TCMT IO Term
checkExpr Expr
e (Type -> TCMT IO Term) -> Type -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
tcm [Term -> Arg Term
forall a. a -> Arg a
hArg Term
lzero, Term -> Arg Term
forall a. a -> Arg a
vArg Term
unit]
  Either UnquoteError (Term, [QName])
res  <- UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM (UnquoteM Term -> TCM (Either UnquoteError (Term, [QName])))
-> UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a b. (a -> b) -> a -> b
$ [QName]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName]
xs ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
-> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> UnquoteM Term
evalTCM Term
m
  case Either UnquoteError (Term, [QName])
res of
    Left UnquoteError
err      -> TypeError -> TCMT IO [QName]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [QName]) -> TypeError -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
    Right (Term
_, [QName]
xs) -> [QName] -> TCMT IO [QName]
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
xs

-- | Instantiate all metas in 'Definition' associated to 'QName'.
--   Makes sense after freezing metas. Some checks, like free variable
--   analysis, are not in 'TCM', so they will be more precise (see issue 1099)
--   after meta instantiation.
--   Precondition: name has been added to signature already.
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType QName
q = do
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl.inst" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"instantiating type of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q
  Type
t  <- Definition -> Type
defType (Definition -> Type)
-> (Signature -> Definition) -> Signature -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe Definition -> Definition
forall a. a -> Maybe a -> a
fromMaybe Definition
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Definition -> Definition)
-> (Signature -> Maybe Definition) -> Signature -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Signature -> Maybe Definition
lookupDefinition QName
q (Signature -> Type) -> TCMT IO Signature -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  Type
t' <- Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Definition -> Definition
updateDefType ((Type -> Type) -> Definition -> Definition)
-> (Type -> Type) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
forall a b. a -> b -> a
const Type
t'
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.inst" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"  t  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , TCM Doc
"  t' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
    ]

-- Andreas, 2014-04-11
-- UNUSED, costs a couple of sec on the std-lib
-- -- | Instantiate all metas in 'Definition' associated to 'QName'.
-- --   Makes sense after freezing metas.
-- --   Some checks, like free variable analysis, are not in 'TCM',
-- --   so they will be more precise (see issue 1099) after meta instantiation.
-- --
-- --   Precondition: name has been added to signature already.
-- instantiateDefinition :: QName -> TCM ()
-- instantiateDefinition q = do
--   reportSLn "tc.decl.inst" 20 $ "instantiating " ++ prettyShow q
--   sig <- getSignature
--   let def = fromMaybe __IMPOSSIBLE__ $ lookupDefinition q sig
--   def <- instantiateFull def
--   modifySignature $ updateDefinition q $ const def

data HighlightModuleContents = DontHightlightModuleContents | DoHighlightModuleContents
  deriving (HighlightModuleContents -> HighlightModuleContents -> Bool
(HighlightModuleContents -> HighlightModuleContents -> Bool)
-> (HighlightModuleContents -> HighlightModuleContents -> Bool)
-> Eq HighlightModuleContents
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
$c/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
== :: HighlightModuleContents -> HighlightModuleContents -> Bool
$c== :: HighlightModuleContents -> HighlightModuleContents -> Bool
Eq)

-- | Highlight a declaration. Called after checking a mutual block (to ensure
--   we have the right definitions for all names). For modules inside mutual
--   blocks we haven't highlighted their contents, but for modules not in a
--   mutual block we have. Hence the flag.
highlight_ :: HighlightModuleContents -> A.Declaration -> TCM ()
highlight_ :: HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
hlmod Declaration
d = do
  let highlight :: Declaration -> TCM ()
highlight Declaration
d = Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
d Level
Full Bool
True
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Declaration
d of
    A.Axiom{}                -> Declaration -> TCM ()
highlight Declaration
d
    A.Field{}                -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Primitive{}            -> Declaration -> TCM ()
highlight Declaration
d
    A.Mutual MutualInfo
i [Declaration]
ds            -> (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
DoHighlightModuleContents) ([Declaration] -> TCM ()) -> [Declaration] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds
    A.Apply{}                -> Declaration -> TCM ()
highlight Declaration
d
    A.Import{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.Pragma{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.ScopedDecl{}           -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    A.FunDef{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.DataDef{}              -> Declaration -> TCM ()
highlight Declaration
d
    A.DataSig{}              -> Declaration -> TCM ()
highlight Declaration
d
    A.Open{}                 -> Declaration -> TCM ()
highlight Declaration
d
    A.PatternSynDef{}        -> Declaration -> TCM ()
highlight Declaration
d
    A.Generalize{}           -> Declaration -> TCM ()
highlight Declaration
d
    A.UnquoteDecl{}          -> Declaration -> TCM ()
highlight Declaration
d
    A.UnquoteDef{}           -> Declaration -> TCM ()
highlight Declaration
d
    A.Section Range
i ModuleName
x GeneralizeTelescope
tel [Declaration]
ds     -> do
      Declaration -> TCM ()
highlight (Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
i ModuleName
x GeneralizeTelescope
tel [])
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HighlightModuleContents
hlmod HighlightModuleContents -> HighlightModuleContents -> Bool
forall a. Eq a => a -> a -> Bool
== HighlightModuleContents
DoHighlightModuleContents) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
hlmod) ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)
    A.RecSig{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs -> Declaration -> TCM ()
highlight (DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
A.noDataDefParams Expr
dummy [Declaration]
cs)
      -- The telescope has already been highlighted.
      where
      -- Andreas, 2016-01-22, issue 1790
      -- The expression denoting the record constructor type
      -- is replace by a dummy expression in order to /not/
      -- generate highlighting from it.
      -- Simply because all the highlighting info is wrong
      -- in the record constructor type:
      -- i) fields become bound variables,
      -- ii) declarations become let-bound variables.
      -- We do not need that crap.
      dummy :: Expr
dummy = ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$
        Text
"do not highlight construct(ed/or) type"

-- | Termination check a declaration.
checkTermination_ :: A.Declaration -> TCM ()
checkTermination_ :: Declaration -> TCM ()
checkTermination_ Declaration
d = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Termination] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDecl: checking termination..."
  -- If there are some termination errors, we throw a warning.
  -- The termination checker already marked non-terminating functions as such.
  TCMT IO Result -> (Result -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (Declaration -> TCMT IO Result
termDecl Declaration
d) ((Result -> TCM ()) -> TCM ()) -> (Result -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Result
termErrs -> do
    Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Result -> Warning
TerminationIssue Result
termErrs

-- | Check a set of mutual names for positivity.
checkPositivity_ :: Info.MutualInfo -> Set QName -> TCM ()
checkPositivity_ :: MutualInfo -> Set QName -> TCM ()
checkPositivity_ MutualInfo
mi Set QName
names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Positivity] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  -- Positivity checking.
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDecl: checking positivity..."
  MutualInfo -> Set QName -> TCM ()
checkStrictlyPositive MutualInfo
mi Set QName
names

  -- Andreas, 2012-02-13: Polarity computation uses information from the
  -- positivity check, so it needs happen after the positivity check.
  [QName] -> TCM ()
forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
 MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
 MonadDebug m, MonadPretty m) =>
[QName] -> m ()
computePolarity ([QName] -> TCM ()) -> [QName] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names

-- | Check that all coinductive records are actually recursive.
--   (Otherwise, one can implement invalid recursion schemes just like
--   for the old coinduction.)
checkCoinductiveRecords :: [A.Declaration] -> TCM ()
checkCoinductiveRecords :: [Declaration] -> TCM ()
checkCoinductiveRecords [Declaration]
ds = [Declaration] -> (Declaration -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Declaration]
ds ((Declaration -> TCM ()) -> TCM ())
-> (Declaration -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \case
  A.RecDef DefInfo
_ QName
q UniverseCheck
_ RecordDirectives
dir DataDefParams
_ Expr
_ [Declaration]
_
    | Just (Ranged Range
r Induction
CoInductive) <- RecordDirectives -> Maybe (Ranged Induction)
forall a. RecordDirectives' a -> Maybe (Ranged Induction)
recInductive RecordDirectives
dir -> Range -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (QName -> TCMT IO Bool
isRecursiveRecord QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$
      VerboseKey
"Only recursive records can be coinductive"
  Declaration
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Check a set of mutual names for constructor-headedness.
checkInjectivity_ :: Set QName -> TCM ()
checkInjectivity_ :: Set QName -> TCM ()
checkInjectivity_ Set QName
names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Injectivity] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDecl: checking injectivity..."
  -- Andreas, 2015-07-01, see Issue1366b:
  -- Injectivity check needs also to be run for abstract definitions.
  -- Fold.forM_ names $ \ q -> ignoreAbstractMode $ do -- NOT NECESSARY after all
  Set QName -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ Set QName
names ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
    -- For abstract q, we should be inAbstractMode,
    -- otherwise getConstInfo returns Axiom.
    --
    -- Andreas, 2015-07-01:
    -- Quite surprisingly, inAbstractMode does not allow us to look
    -- at a local definition (@where@ block) of an abstract definition.
    -- This is because the local definition is defined in a strict submodule.
    -- We can only see through abstract definitions in the current module
    -- or super modules inAbstractMode.
    -- I changed that in Monad.Signature.treatAbstractly', so we can see
    -- our own local definitions.
    case Definition -> Defn
theDef Definition
def of
      d :: Defn
d@Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funTerminates :: Defn -> Maybe Bool
funTerminates = Maybe Bool
term, funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
mproj }
        | Maybe Bool
term Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True -> do
            -- Not terminating, thus, running the injectivity check could get us into a loop.
            VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.check" VerboseLevel
35 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is not verified as terminating, thus, not considered for injectivity"
        | Defn -> Bool
isProperProjection Defn
d -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.check" VerboseLevel
40 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is a projection, thus, not considered for injectivity"
        | Bool
otherwise -> do

            FunctionInverse
inv <- QName -> [Clause] -> TCM FunctionInverse
checkInjectivity QName
q [Clause]
cs
            (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Defn -> Defn -> Defn
forall a b. a -> b -> a
const (Defn -> Defn -> Defn) -> Defn -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
              Defn
d { funInv :: FunctionInverse
funInv = FunctionInverse
inv }

      Defn
_ -> do
        AbstractMode
abstr <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.check" VerboseLevel
40 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
          VerboseKey
"we are in " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ AbstractMode -> VerboseKey
forall a. Show a => a -> VerboseKey
show AbstractMode
abstr VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" and " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
             QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is abstract or not a function, thus, not considered for injectivity"

-- | Check a set of mutual names for projection likeness.
--
--   Only a single, non-abstract function can be projection-like.
--   Making an abstract function projection-like would break the
--   invariant that the type of the principle argument of a projection-like
--   function is always inferable.

checkProjectionLikeness_ :: Set QName -> TCM ()
checkProjectionLikeness_ :: Set QName -> TCM ()
checkProjectionLikeness_ Set QName
names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.ProjectionLikeness] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      -- Non-mutual definitions can be considered for
      -- projection likeness
      let ds :: [QName]
ds = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkDecl: checking projection-likeness of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [QName] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [QName]
ds
      case [QName]
ds of
        [QName
d] -> do
          Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          -- For abstract identifiers, getConstInfo returns Axiom.
          -- Thus, abstract definitions are not considered for projection-likeness.
          case Definition -> Defn
theDef Definition
def of
            Function{} -> QName -> TCM ()
makeProjection (Definition -> QName
defName Definition
def)
            Defn
_          -> VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" VerboseLevel
25 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
d VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is abstract or not a function, thus, not considered for projection-likeness"
        [QName]
_ -> VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" VerboseLevel
25 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
               VerboseKey
"mutual definitions are not considered for projection-likeness"

-- | Freeze metas created by given computation if in abstract mode.
whenAbstractFreezeMetasAfter :: A.DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter :: DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter Info.DefInfo{ Access
defAccess :: forall t. DefInfo' t -> Access
defAccess :: Access
defAccess, IsAbstract
defAbstract :: forall t. DefInfo' t -> IsAbstract
defAbstract :: IsAbstract
defAbstract} TCM a
m = do
  if IsAbstract
defAbstract IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
/= IsAbstract
AbstractDef then TCM a
m else do
    (a
a, MetaStore
ms) <- TCM a -> TCMT IO (a, MetaStore)
forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy TCM a
m
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Attempting to solve constraints before freezing."
    TCM ()
wakeupConstraints_   -- solve emptiness and instance constraints
    IntSet
xs <- MetaStore -> TCMT IO IntSet
freezeMetas MetaStore
ms
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.ax" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"Abstract type signature produced new metas: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((VerboseLevel -> TCM Doc) -> [VerboseLevel] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([VerboseLevel] -> [TCM Doc]) -> [VerboseLevel] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ MetaStore -> [VerboseLevel]
forall a. IntMap a -> [VerboseLevel]
IntMap.keys MetaStore
ms)
      , TCM Doc
"We froze the following ones of these:       " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((VerboseLevel -> TCM Doc) -> [VerboseLevel] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([VerboseLevel] -> [TCM Doc]) -> [VerboseLevel] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ IntSet -> [VerboseLevel]
IntSet.toList IntSet
xs)
      ]
    a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

checkGeneralize :: Set QName -> A.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
checkGeneralize :: Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
checkGeneralize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e = do

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.gen" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"checking type signature of generalizable variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
      ]

    -- Check the signature and collect the created metas.
    ([Maybe QName]
telNames, Type
tGen) <-
      Set QName -> TCMT IO Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s (TCMT IO Type -> TCM ([Maybe QName], Type))
-> TCMT IO Type -> TCM ([Maybe QName], Type)
forall a b. (a -> b) -> a -> b
$ Lens' DoGeneralize TCEnv
-> (DoGeneralize -> DoGeneralize) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' DoGeneralize TCEnv
eGeneralizeMetas (DoGeneralize -> DoGeneralize -> DoGeneralize
forall a b. a -> b -> a
const DoGeneralize
YesGeneralizeMeta) (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
        TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
    let n :: VerboseLevel
n = [Maybe QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Maybe QName]
telNames

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.gen" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"checked type signature of generalizable variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
tGen
      ]

    Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
    QName -> Definition -> TCM ()
addConstant QName
x (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
info QName
x Type
tGen Language
lang Defn
GeneralizableVar)
                    { defArgGeneralizable :: NumGeneralizableArgs
defArgGeneralizable = VerboseLevel -> NumGeneralizableArgs
SomeGeneralizableArgs VerboseLevel
n }


-- | Type check an axiom.
checkAxiom :: KindOfName -> A.DefInfo -> ArgInfo ->
              Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom :: KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> TCM ()
checkAxiom = Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
forall a. Maybe a
Nothing

-- | Data and record type signatures need to remember the generalized
--   parameters for when checking the corresponding definition, so for these we
--   pass in the parameter telescope separately.
checkAxiom' :: Maybe A.GeneralizeTelescope -> KindOfName -> A.DefInfo -> ArgInfo ->
               Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom' :: Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
gentel KindOfName
kind DefInfo
i ArgInfo
info0 Maybe [Occurrence]
mp QName
x Expr
e = DefInfo -> TCM () -> TCM ()
forall a. DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  -- Andreas, 2016-07-19 issues #418 #2102:
  -- We freeze metas in type signatures of abstract definitions, to prevent
  -- leakage of implementation details.

  -- Andreas, 2012-04-18  if we are in irrelevant context, axioms are irrelevant
  -- even if not declared as such (Issue 610).
  -- Andreas, 2019-06-17  also for erasure (issue #3855).
  Relevance
rel <- Relevance -> Relevance -> Relevance
forall a. Ord a => a -> a -> a
max (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info0) (Relevance -> Relevance) -> TCMT IO Relevance -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
  Quantity
q   <- (TCEnv -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity TCMT IO Quantity -> (Quantity -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    q :: Quantity
q@Quantity0{} -> Quantity
q
    Quantity
_ -> ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info0

  -- Andrea, 2019-07-16 Cohesion is purely based on left-division, it
  -- does not take envModality into account.
  let c :: Cohesion
c = ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info0
  let mod :: Modality
mod  = Relevance -> Quantity -> Cohesion -> Modality
Modality Relevance
rel Quantity
q Cohesion
c
  let info :: ArgInfo
info = Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info0
  Cohesion -> TCM () -> TCM ()
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.ax" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checking type signature"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Modality -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Maybe GeneralizeTelescope
-> TCM Doc -> (GeneralizeTelescope -> TCM Doc) -> TCM Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe GeneralizeTelescope
gentel TCM Doc
"(no gentel)" ((GeneralizeTelescope -> TCM Doc) -> TCM Doc)
-> (GeneralizeTelescope -> TCM Doc) -> TCM Doc
forall a b. (a -> b) -> a -> b
$ \ GeneralizeTelescope
_ -> TCM Doc
"(has gentel)"
    ]

  ([Maybe Name]
genParams, VerboseLevel
npars, Type
t) <- TCMT IO ([Maybe Name], VerboseLevel, Type)
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO ([Maybe Name], VerboseLevel, Type)
 -> TCMT IO ([Maybe Name], VerboseLevel, Type))
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall a b. (a -> b) -> a -> b
$ case Maybe GeneralizeTelescope
gentel of
        Maybe GeneralizeTelescope
Nothing     -> ([], VerboseLevel
0,) (Type -> ([Maybe Name], VerboseLevel, Type))
-> TCMT IO Type -> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Type
isType_ Expr
e
        Just GeneralizeTelescope
gentel ->
          GeneralizeTelescope
-> ([Maybe Name]
    -> Telescope -> TCMT IO ([Maybe Name], VerboseLevel, Type))
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall a.
GeneralizeTelescope
-> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope GeneralizeTelescope
gentel (([Maybe Name]
  -> Telescope -> TCMT IO ([Maybe Name], VerboseLevel, Type))
 -> TCMT IO ([Maybe Name], VerboseLevel, Type))
-> ([Maybe Name]
    -> Telescope -> TCMT IO ([Maybe Name], VerboseLevel, Type))
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall a b. (a -> b) -> a -> b
$ \ [Maybe Name]
genParams Telescope
ptel -> do
            Type
t <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
            ([Maybe Name], VerboseLevel, Type)
-> TCMT IO ([Maybe Name], VerboseLevel, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe Name]
genParams, Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ptel, Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
ptel Type
t)

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.ax" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checked type signature"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Modality -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"of sort " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t)
    ]

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Maybe Name] -> Bool
forall a. Null a => a -> Bool
null [Maybe Name]
genParams) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl.ax" VerboseLevel
40 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  generalized params: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Maybe Name] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [Maybe Name]
genParams

  -- Jesper, 2018-06-05: should be done AFTER generalizing
  --whenM (optDoubleCheck <$> pragmaOptions) $ workOnTypes $ do
  --  checkInternal (unEl t) (sort $ getSort t)

  -- Andreas, 2015-03-17 Issue 1428: Do not postulate sizes in parametrized
  -- modules!
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (KindOfName
kind KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
AxiomName) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Sort' Term -> Sort' Term -> Bool
forall a. Eq a => a -> a -> Bool
== Sort' Term
forall t. Sort' t
SizeUniv) (Sort' Term -> Bool) -> TCMT IO (Sort' Term) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Sort' Term -> TCMT IO (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort' Term -> TCMT IO (Sort' Term))
-> Sort' Term -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0) (VerboseLevel -> Bool) -> TCMT IO VerboseLevel -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"We don't like postulated sizes in parametrized modules."

  -- Ensure that polarity pragmas do not contain too many occurrences.
  ([Occurrence]
occs, [Polarity]
pols) <- case Maybe [Occurrence]
mp of
    Maybe [Occurrence]
Nothing   -> ([Occurrence], [Polarity]) -> TCMT IO ([Occurrence], [Polarity])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    Just [Occurrence]
occs -> do
      TelV Telescope
tel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
      let n :: VerboseLevel
n = [Dom (VerboseKey, Type)] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel)
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< [Occurrence] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Occurrence]
occs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> VerboseLevel -> TypeError
TooManyPolarities QName
x VerboseLevel
n
      let pols :: [Polarity]
pols = (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc [Occurrence]
occs
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.polarity.pragma" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
        VerboseKey
"Setting occurrences and polarity for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
":\n  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
        [Occurrence] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Occurrence]
occs VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pols
      ([Occurrence], [Polarity]) -> TCMT IO ([Occurrence], [Polarity])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Occurrence]
occs, [Polarity]
pols)


  -- Set blocking tag to MissingClauses if we still expect clauses
  let blk :: Blocked' Term ()
blk = case KindOfName
kind of
        KindOfName
FunName   -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
MissingClauses   ()
        KindOfName
MacroName -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
MissingClauses   ()
        KindOfName
_         -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()

  -- Not safe. See Issue 330
  -- t <- addForcingAnnotations t

  Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
  let defn :: Definition
defn = ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
info QName
x Type
t Language
lang (Defn -> Definition) -> Defn -> Definition
forall a b. (a -> b) -> a -> b
$
        case KindOfName
kind of   -- #4833: set abstract already here so it can be inherited by with functions
          KindOfName
FunName   -> Defn
emptyFunction{ funAbstr :: IsAbstract
funAbstr = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i }
          KindOfName
MacroName -> Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro Bool
True Defn
emptyFunction{ funAbstr :: IsAbstract
funAbstr = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i }
          KindOfName
DataName  -> VerboseLevel -> Defn
DataOrRecSig VerboseLevel
npars
          KindOfName
RecName   -> VerboseLevel -> Defn
DataOrRecSig VerboseLevel
npars
          KindOfName
AxiomName -> Defn
defaultAxiom     -- Old comment: NB: used also for data and record type sigs
          KindOfName
_         -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

  QName -> Definition -> TCM ()
addConstant QName
x (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ Definition
defn
        { defArgOccurrences :: [Occurrence]
defArgOccurrences    = [Occurrence]
occs
        , defPolarity :: [Polarity]
defPolarity          = [Polarity]
pols
        , defGeneralizedParams :: [Maybe Name]
defGeneralizedParams = [Maybe Name]
genParams
        , defBlocked :: Blocked' Term ()
defBlocked           = Blocked' Term ()
blk
        }

  -- Add the definition to the instance table, if needed
  case DefInfo -> IsInstance
forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
    InstanceDef Range
_r -> QName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCM ()
addTypedInstance QName
x Type
t
      -- Put highlighting on name only; including the instance keyword,
      -- like @(getRange (r,x))@, does not produce good results.
    IsInstance
NotInstanceDef -> () -> TCM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
IsType_ Expr
e) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do -- need Range for error message
    -- Andreas, 2016-06-21, issue #2054
    -- Do not default size metas to ∞ in local type signatures
    Bool
checkingWhere <- (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckingWhere
    DefaultToInfty -> TCM ()
solveSizeConstraints (DefaultToInfty -> TCM ()) -> DefaultToInfty -> TCM ()
forall a b. (a -> b) -> a -> b
$ if Bool
checkingWhere then DefaultToInfty
DontDefaultToInfty else DefaultToInfty
DefaultToInfty

-- | Type check a primitive function declaration.
checkPrimitive :: A.DefInfo -> QName -> Arg A.Expr -> TCM ()
checkPrimitive :: DefInfo -> QName -> Arg Expr -> TCM ()
checkPrimitive DefInfo
i QName
x (Arg ArgInfo
info Expr
e) =
    Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Expr -> Call
CheckPrimitive (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
x Expr
e) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (VerboseKey
name, PrimImpl Type
t' PrimFun
pf) <- QName -> TCM (VerboseKey, PrimitiveImpl)
lookupPrimitiveFunctionQ QName
x
    -- Certain "primitive" functions are BUILTIN rather than
    -- primitive.
    let builtinPrimitives :: [VerboseKey]
builtinPrimitives =
          [ VerboseKey
"primNatPlus"
          , VerboseKey
"primNatMinus"
          , VerboseKey
"primNatTimes"
          , VerboseKey
"primNatDivSucAux"
          , VerboseKey
"primNatModSucAux"
          , VerboseKey
"primNatEquality"
          , VerboseKey
"primNatLess"
          , VerboseKey
"primLevelZero"
          , VerboseKey
"primLevelSuc"
          , VerboseKey
"primLevelMax"
          , VerboseKey
"primSetOmega"
          , VerboseKey
"primStrictSet"
          , VerboseKey
"primStrictSetOmega"
          ]
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VerboseKey
name VerboseKey -> [VerboseKey] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VerboseKey]
builtinPrimitives) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.prim" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
name TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"is a BUILTIN, not a primitive!"
      TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
NoSuchPrimitiveFunction VerboseKey
name
    Type
t <- Expr -> TCMT IO Type
isType_ Expr
e
    TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t Type
t'
    let s :: VerboseKey
s  = Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> VerboseKey) -> Name -> VerboseKey
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
    -- Checking the modality. Currently all primitives require default
    -- modalities, and likely very few will have different modalities in the
    -- future. Thus, rather than, the arguably nicer solution of adding a
    -- modality to PrimImpl we simply check the few special primitives here.
    let expectedInfo :: ArgInfo
expectedInfo =
          case VerboseKey
name of
            -- Currently no special primitives
            VerboseKey
_ -> ArgInfo
defaultArgInfo
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ArgInfo
info ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
expectedInfo) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> ArgInfo -> ArgInfo -> TypeError
WrongModalityForPrimitive VerboseKey
name ArgInfo
info ArgInfo
expectedInfo
    VerboseKey -> PrimFun -> TCM ()
bindPrimitive VerboseKey
s PrimFun
pf
    QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
x ArgInfo
info QName
x Type
t (Defn -> TCM ()) -> Defn -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Primitive :: IsAbstract
-> VerboseKey
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive { primAbstr :: IsAbstract
primAbstr    = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
                  , primName :: VerboseKey
primName     = VerboseKey
s
                  , primClauses :: [Clause]
primClauses  = []
                  , primInv :: FunctionInverse
primInv      = FunctionInverse
forall c. FunctionInverse' c
NotInjective
                  , primCompiled :: Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
forall a. Maybe a
Nothing }

-- | Check a pragma.
checkPragma :: Range -> A.Pragma -> TCM ()
checkPragma :: Range -> Pragma -> TCM ()
checkPragma Range
r Pragma
p =
    Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> Pragma -> Call
CheckPragma Range
r Pragma
p) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Pragma
p of
        A.BuiltinPragma RString
rb ResolvedName
x
          | VerboseKey -> Bool
isUntypedBuiltin VerboseKey
b -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          | Bool
otherwise          -> VerboseKey -> ResolvedName -> TCM ()
bindBuiltin VerboseKey
b ResolvedName
x
          where b :: VerboseKey
b = RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
rb
        A.BuiltinNoDefPragma RString
b KindOfName
_kind QName
x -> VerboseKey -> QName -> TCM ()
bindBuiltinNoDef (RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
b) QName
x
        A.RewritePragma Range
_ [QName]
qs -> [QName] -> TCM ()
addRewriteRules [QName]
qs
        A.CompilePragma RString
b QName
x VerboseKey
s -> do
          -- Check that x resides in the same module (or a child) as the pragma.
          QName
x' <- Definition -> QName
defName (Definition -> QName) -> TCMT IO Definition -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x  -- Get the canonical name of x.
          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((QName
x' QName -> ModuleName -> Bool
`isInModule`) (ModuleName -> Bool) -> TCMT IO ModuleName -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$
              VerboseKey
"COMPILE pragmas must appear in the same module as their corresponding definitions,"
          VerboseKey -> QName -> VerboseKey -> TCM ()
addPragma (RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
b) QName
x VerboseKey
s
        A.StaticPragma QName
x -> do
          Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          case Definition -> Defn
theDef Definition
def of
            Function{} -> QName -> TCM ()
markStatic QName
x
            Defn
_          -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError VerboseKey
"STATIC directive only works on functions"
        A.InjectivePragma QName
x -> QName -> TCM ()
markInjective QName
x
        A.InlinePragma Bool
b QName
x -> do
          Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          case Definition -> Defn
theDef Definition
def of
            Function{} -> Bool -> QName -> TCM ()
markInline Bool
b QName
x
            Defn
_          -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
sINLINE VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" directive only works on functions"
              where sINLINE :: VerboseKey
sINLINE = if Bool
b then VerboseKey
"INLINE" else VerboseKey
"NOINLINE"
        A.OptionsPragma{} -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"OPTIONS pragma only allowed at beginning of file, before top module declaration"
        A.DisplayPragma QName
f [NamedArg Pattern]
ps Expr
e -> QName -> [NamedArg Pattern] -> Expr -> TCM ()
checkDisplayPragma QName
f [NamedArg Pattern]
ps Expr
e
        A.EtaPragma QName
r -> do
          let noRecord :: TCMT IO a
noRecord = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$
                VerboseKey
"ETA pragma is only applicable to coinductive records"
          TCMT IO (Maybe Defn) -> TCM () -> (Defn -> TCM ()) -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> TCMT IO (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) TCM ()
forall a. TCMT IO a
noRecord ((Defn -> TCM ()) -> TCM ()) -> (Defn -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \case
            Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality
eta } -> do
              Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe Induction
ind Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
== Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. TCMT IO a
noRecord
              if | Specified NoEta{} <- EtaEquality
eta -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$
                     VerboseKey
"ETA pragma conflicts with no-eta-equality declaration"
                 | Bool
otherwise -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Defn
_ -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
r ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
            def :: Defn
def@Record{} -> Defn
def { recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta' PatternOrCopattern -> EtaEquality
Specified HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta }
            Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Type check a bunch of mutual inductive recursive definitions.
--
-- All definitions which have so far been assigned to the given mutual
-- block are returned.
checkMutual :: Info.MutualInfo -> [A.Declaration] -> TCM (MutualId, Set QName)
checkMutual :: MutualInfo -> [Declaration] -> TCMT IO (MutualId, Set QName)
checkMutual MutualInfo
i [Declaration]
ds = (MutualId -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName)
forall a. (MutualId -> TCM a) -> TCM a
inMutualBlock ((MutualId -> TCMT IO (MutualId, Set QName))
 -> TCMT IO (MutualId, Set QName))
-> (MutualId -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName)
forall a b. (a -> b) -> a -> b
$ \ MutualId
blockId -> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero (TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
forall a b. (a -> b) -> a -> b
$ do

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl.mutual" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      ((TCM Doc
"Checking mutual block" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (MutualId -> VerboseKey
forall a. Show a => a -> VerboseKey
show MutualId
blockId)) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":") TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
:
      (Declaration -> TCM Doc) -> [Declaration] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc)
-> (Declaration -> TCM Doc) -> Declaration -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA) [Declaration]
ds

  MutualId -> MutualInfo -> TCM ()
insertMutualBlockInfo MutualId
blockId MutualInfo
i
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ( Lens' (TerminationCheck ()) TCEnv
-> LensSet (TerminationCheck ()) TCEnv
forall i o. Lens' i o -> LensSet i o
set Lens' (TerminationCheck ()) TCEnv
eTerminationCheck (() () -> TerminationCheck Name -> TerminationCheck ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ MutualInfo -> TerminationCheck Name
Info.mutualTerminationCheck MutualInfo
i)
          (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' CoverageCheck TCEnv -> LensSet CoverageCheck TCEnv
forall i o. Lens' i o -> LensSet i o
set Lens' CoverageCheck TCEnv
eCoverageCheck (MutualInfo -> CoverageCheck
Info.mutualCoverageCheck MutualInfo
i)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDecl [Declaration]
ds

  (MutualId
blockId, ) (Set QName -> (MutualId, Set QName))
-> (MutualBlock -> Set QName)
-> MutualBlock
-> (MutualId, Set QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MutualBlock -> Set QName
mutualNames (MutualBlock -> (MutualId, Set QName))
-> TCMT IO MutualBlock -> TCMT IO (MutualId, Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> TCMT IO MutualBlock
lookupMutualBlock MutualId
blockId

-- | Type check the type signature of an inductive or recursive definition.
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature :: Declaration -> TCM ()
checkTypeSignature = Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
forall a. Maybe a
Nothing

checkTypeSignature' :: Maybe A.GeneralizeTelescope -> A.TypeSignature -> TCM ()
checkTypeSignature' :: Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
gtel (A.ScopedDecl ScopeInfo
scope [Declaration]
ds) = do
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
gtel) [Declaration]
ds
checkTypeSignature' Maybe GeneralizeTelescope
gtel (A.Axiom KindOfName
funSig DefInfo
i ArgInfo
info Maybe [Occurrence]
mp QName
x Expr
e) =
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.TypeSig] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    let abstr :: TCM () -> TCM ()
abstr = case DefInfo -> Access
forall t. DefInfo' t -> Access
Info.defAccess DefInfo
i of
          PrivateAccess{}
            | DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
              -- Issue #2321, only go to AbstractMode for abstract definitions
              -- Issue #418, #3744, in fact don't go to AbstractMode at all
            | Bool
otherwise -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
          Access
PublicAccess  -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    in TCM () -> TCM ()
abstr (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
gtel KindOfName
funSig DefInfo
i ArgInfo
info Maybe [Occurrence]
mp QName
x Expr
e
checkTypeSignature' Maybe GeneralizeTelescope
_ Declaration
_ =
  TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__   -- type signatures are always axioms


-- | Type check a module.

checkSection :: ModuleName -> A.GeneralizeTelescope -> [A.Declaration] -> TCM ()
checkSection :: ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
checkSection ModuleName
x GeneralizeTelescope
tel [Declaration]
ds = ModuleName -> GeneralizeTelescope -> TCM () -> TCM ()
forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection ModuleName
x GeneralizeTelescope
tel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds


-- | Helper for 'checkSectionApplication'.
--
--   Matches the arguments of the module application with the
--   module parameters.
--
--   Returns the remaining module parameters as an open telescope.
--   Warning: the returned telescope is /not/ the final result,
--   an actual instantiation of the parameters does not occur.
checkModuleArity
  :: ModuleName           -- ^ Name of applied module.
  -> Telescope            -- ^ The module parameters.
  -> [NamedArg A.Expr]  -- ^ The arguments this module is applied to.
  -> TCM Telescope        -- ^ The remaining module parameters (has free de Bruijn indices!).
checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope
checkModuleArity ModuleName
m Telescope
tel [NamedArg Expr]
args = Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
  where
    bad :: TCM Telescope
bad = TypeError -> TCM Telescope
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Telescope) -> TypeError -> TCM Telescope
forall a b. (a -> b) -> a -> b
$ ModuleName -> Telescope -> [NamedArg Expr] -> TypeError
ModuleArityMismatch ModuleName
m Telescope
tel [NamedArg Expr]
args

    check :: Telescope -> [NamedArg A.Expr] -> TCM Telescope
    check :: Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel []             = Telescope -> TCM Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
tel
    check Telescope
EmptyTel (NamedArg Expr
_:[NamedArg Expr]
_)     = TCM Telescope
bad
    check (ExtendTel dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} Abs Telescope
btel) args0 :: [NamedArg Expr]
args0@(Arg ArgInfo
info' Named_ Expr
arg : [NamedArg Expr]
args) =
      let name :: Maybe VerboseKey
name = Named_ Expr -> Maybe VerboseKey
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
a -> Maybe VerboseKey
bareNameOf Named_ Expr
arg
          my :: Maybe VerboseKey
my   = Dom Type -> Maybe VerboseKey
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
a -> Maybe VerboseKey
bareNameOf Dom Type
dom
          tel :: Telescope
tel  = Abs Telescope -> Telescope
forall a. Subst a => Abs a -> a
absBody Abs Telescope
btel in
      case (ArgInfo -> Hiding
argInfoHiding ArgInfo
info, ArgInfo -> Hiding
argInfoHiding ArgInfo
info', Maybe VerboseKey
name) of
        (Instance{}, Hiding
NotHidden, Maybe VerboseKey
_)        -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Instance{}, Hiding
Hidden, Maybe VerboseKey
_)           -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Instance{}, Instance{}, Maybe VerboseKey
Nothing) -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
        (Instance{}, Instance{}, Just VerboseKey
x)
          | VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just VerboseKey
x Maybe VerboseKey -> Maybe VerboseKey -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe VerboseKey
my                  -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Hiding
NotHidden, Maybe VerboseKey
_)            -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Instance{}, Maybe VerboseKey
_)           -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Hiding
Hidden, Maybe VerboseKey
Nothing)         -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
        (Hiding
Hidden, Hiding
Hidden, Just VerboseKey
x)
          | VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just VerboseKey
x Maybe VerboseKey -> Maybe VerboseKey -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe VerboseKey
my                  -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args0
        (Hiding
NotHidden, Hiding
NotHidden, Maybe VerboseKey
_)         -> Telescope -> [NamedArg Expr] -> TCM Telescope
check Telescope
tel [NamedArg Expr]
args
        (Hiding
NotHidden, Hiding
Hidden, Maybe VerboseKey
_)            -> TCM Telescope
bad
        (Hiding
NotHidden, Instance{}, Maybe VerboseKey
_)        -> TCM Telescope
bad

-- | Check an application of a section.
checkSectionApplication
  :: Info.ModuleInfo
  -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
  -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
  -> A.ScopeCopyInfo     -- ^ Imported names and modules
  -> TCM ()
checkSectionApplication :: ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
copyInfo =
  Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> ModuleName -> ModuleApplication -> Call
CheckSectionApplication (ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i) ModuleName
m1 ModuleApplication
modapp) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
  -- A section application is type-checked in a non-erased context
  -- (#5410).
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' Quantity TCEnv -> LensMap Quantity TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Quantity TCEnv
eQuantity LensMap Quantity TCEnv -> LensMap Quantity TCEnv
forall a b. (a -> b) -> a -> b
$ (Quantity -> Quantity) -> Quantity -> Quantity
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
`addQuantity` Quantity
topQuantity)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
  ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication' ModuleInfo
i ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
copyInfo

-- | Check an application of a section. (Do not invoke this procedure
-- directly, use 'checkSectionApplication'.)
checkSectionApplication'
  :: Info.ModuleInfo
  -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
  -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
  -> A.ScopeCopyInfo     -- ^ Imported names and modules
  -> TCM ()
checkSectionApplication' :: ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication' ModuleInfo
i ModuleName
m1 (A.SectionApp Telescope
ptel ModuleName
m2 [NamedArg Expr]
args) ScopeCopyInfo
copyInfo = do
  -- Module applications can appear in lets, in which case we treat
  -- lambda-bound variables as additional parameters to the module.
  VerboseLevel
extraParams <- do
    VerboseLevel
mfv <- TCMT IO VerboseLevel
getCurrentModuleFreeVars
    VerboseLevel
fv  <- TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
    VerboseLevel -> TCMT IO VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
fv VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
mfv)
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VerboseLevel
extraParams VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.mod.apply" VerboseLevel
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Extra parameters to " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ModuleName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow ModuleName
m1 VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
": " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
extraParams
  -- Type-check the LHS (ptel) of the module macro.
  Telescope -> (Telescope -> TCM ()) -> TCM ()
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope Telescope
ptel ((Telescope -> TCM ()) -> TCM ())
-> (Telescope -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Telescope
ptel -> do
    -- We are now in the context @ptel@.
    -- Get the correct parameter telescope of @m2@. This is the fully lifted
    -- telescope obtained by `lookupSection` instantiated with the module
    -- parameters of `m2` currently in scope. For instance
    -- ```
    --  module _ (A : Set) where
    --    module M (B : Set) where ...
    --    module M' = M B
    -- ```
    -- In the application `M' = M B`, `tel = (A B : Set)` and
    -- `moduleParamsToApply M = [A]`, so the resulting parameter telescope is
    -- `tel' = (B : Set)`.
    Telescope
tel <- ModuleName -> TCM Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m2
    Args
vs  <- ModuleName -> TCMT IO Args
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m Args
moduleParamsToApply ModuleName
m2
    let tel' :: Telescope
tel'  = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
vs
    -- Compute the remaining parameter telescope after stripping of
    -- the initial parameters that are determined by the @args@.
    -- Warning: @etaTel@ is not well-formed in @ptel@, since
    -- the actual application has not happened.
    Telescope
etaTel <- ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope
checkModuleArity ModuleName
m2 Telescope
tel' [NamedArg Expr]
args
    -- Take the module parameters that will be instantiated by @args@.
    let tel'' :: Telescope
tel'' = [Dom (VerboseKey, Type)] -> Telescope
telFromList ([Dom (VerboseKey, Type)] -> Telescope)
-> [Dom (VerboseKey, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. VerboseLevel -> [a] -> [a]
take (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel' VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
etaTel) ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)])
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel'
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"applying section" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m2
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"args =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((NamedArg Expr -> TCM Doc) -> [NamedArg Expr] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Expr -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Expr]
args)
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ptel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ptel) (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ptel)
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel' =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel''=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel''
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"eta  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ptel) (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel'' (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
etaTel)
      ]
    -- Now, type check arguments.
    Args
ts <- TCMT IO (Elims, Telescope) -> TCMT IO (Elims, Telescope)
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Telescope
-> TCMT IO (Elims, Telescope)
checkArguments_ Comparison
CmpEq ExpandHidden
DontExpandLast (ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i) [NamedArg Expr]
args Telescope
tel') TCMT IO (Elims, Telescope)
-> ((Elims, Telescope) -> TCMT IO Args) -> TCMT IO Args
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (Elims
ts', Telescope
etaTel') | (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
etaTel VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
etaTel')
                     , Just Args
ts <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
ts' -> Args -> TCMT IO Args
forall (m :: * -> *) a. Monad m => a -> m a
return Args
ts
      (Elims, Telescope)
_ -> TCMT IO Args
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Perform the application of the module parameters.
    let aTel :: Telescope
aTel = Telescope
tel' Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
ts
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"aTel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
aTel
      ]
    -- Andreas, 2014-04-06, Issue 1094:
    -- Add the section with well-formed telescope.
    KeepNames Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope -> KeepNames Telescope
forall a. a -> KeepNames a
KeepNames Telescope
aTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"addSection" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m1 TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCM Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope TCM Telescope -> (Telescope -> TCM Doc) -> TCM Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Telescope
tel -> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel))
      ModuleName -> TCM ()
addSection ModuleName
m1

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"applySection", ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m1, TCM Doc
"=", ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m2, [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
ts) ]
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ScopeCopyInfo -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ScopeCopyInfo
copyInfo
      ]
    Args
args <- Args -> TCMT IO Args
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Args -> TCMT IO Args) -> Args -> TCMT IO Args
forall a b. (a -> b) -> a -> b
$ Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
ts
    let n :: VerboseLevel
n = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
aTel
    Args
etaArgs <- TCMT IO Args -> TCMT IO Args
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Args -> TCMT IO Args) -> TCMT IO Args -> TCMT IO Args
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Args -> TCMT IO Args
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
aTel TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    KeepNames Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope -> KeepNames Telescope
forall a. a -> KeepNames a
KeepNames Telescope
aTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      ModuleName
-> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection ModuleName
m1 (Telescope
ptel Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
aTel) ModuleName
m2 (VerboseLevel -> Args -> Args
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
n Args
args Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
etaArgs) ScopeCopyInfo
copyInfo

checkSectionApplication' ModuleInfo
i ModuleName
m1 (A.RecordModuleInstance ModuleName
x) ScopeCopyInfo
copyInfo = do
  let name :: QName
name = ModuleName -> QName
mnameToQName ModuleName
x
  Telescope
tel' <- ModuleName -> TCM Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
x
  Args
vs   <- ModuleName -> TCMT IO Args
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m Args
moduleParamsToApply ModuleName
x
  let tel :: Telescope
tel = Telescope
tel' Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
vs
      args :: Args
args = Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel

      telInst :: Telescope
      telInst :: Telescope
telInst = Telescope -> Telescope
instFinal Telescope
tel

      -- Locate last (rightmost) parameter and make it @Instance@.
      -- Issue #3463: also name it so it can be given by name.
      instFinal :: Telescope -> Telescope
      -- Telescopes do not have @NoAbs@.
      instFinal :: Telescope -> Telescope
instFinal (ExtendTel Dom Type
_ NoAbs{}) = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Found last parameter: switch it to @Instance@.
      instFinal (ExtendTel Dom Type
dom (Abs VerboseKey
n Telescope
EmptyTel)) =
                 Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
do' (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
n Telescope
forall a. Tele a
EmptyTel)
        where do' :: Dom Type
do' = Dom Type -> Dom Type
forall a. LensHiding a => a -> a
makeInstance Dom Type
dom { domName :: Maybe NamedName
domName = NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> RString -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (RString -> NamedName) -> RString -> NamedName
forall a b. (a -> b) -> a -> b
$ VerboseKey -> RString
forall a. a -> Ranged a
unranged VerboseKey
"r" }
      -- Otherwise, keep searchinf for last parameter:
      instFinal (ExtendTel Dom Type
arg (Abs VerboseKey
n Telescope
tel)) =
                 Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
arg (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
n (Telescope -> Telescope
instFinal Telescope
tel))
      -- Before instFinal is invoked, we have checked that the @tel@ is not empty.
      instFinal Telescope
EmptyTel = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"applySection", QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name, TCM Doc
"{{...}}" ]
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"x       =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
x
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"name    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"telInst =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
telInst
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
    -- , nest 2 $ "args    =" <+> sep (map prettyTCM args)
    ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Args -> VerboseKey
forall a. Show a => a -> VerboseKey
show Args
vs)
    -- , nest 2 $ "args    =" <+> text (show args)
    ]
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope
tel Telescope -> Telescope -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope
forall a. Tele a
EmptyTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (QName -> QName
qnameToConcrete QName
name) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is not a parameterised section"

  Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
telInst (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    Args
vs <- ModuleName -> TCMT IO Args
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m Args
moduleParamsToApply ModuleName
x
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"args    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCM Doc -> TCM Doc)
-> (Arg Term -> TCM Doc) -> Arg Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) Args
args)
      ]
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.mod.apply" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Args -> VerboseKey
forall a. Show a => a -> VerboseKey
show Args
vs)
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"args    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Args -> VerboseKey
forall a. Show a => a -> VerboseKey
show Args
args)
      ]
    ModuleName -> TCM ()
addSection ModuleName
m1
    ModuleName
-> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection ModuleName
m1 Telescope
telInst ModuleName
x (Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
args) ScopeCopyInfo
copyInfo

-- | Type check an import declaration. Actually doesn't do anything, since all
--   the work is done when scope checking.
checkImport :: Info.ModuleInfo -> ModuleName -> TCM ()
checkImport :: ModuleInfo -> ModuleName -> TCM ()
checkImport ModuleInfo
i ModuleName
x = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

------------------------------------------------------------------------
-- * Debugging
------------------------------------------------------------------------

class ShowHead a where
  showHead :: a -> String

instance ShowHead A.Declaration where
  showHead :: Declaration -> VerboseKey
showHead Declaration
d =
    case Declaration
d of
      A.Axiom        {} -> VerboseKey
"Axiom"
      A.Field        {} -> VerboseKey
"Field"
      A.Primitive    {} -> VerboseKey
"Primitive"
      A.Mutual       {} -> VerboseKey
"Mutual"
      A.Section      {} -> VerboseKey
"Section"
      A.Apply        {} -> VerboseKey
"Apply"
      A.Import       {} -> VerboseKey
"Import"
      A.Pragma       {} -> VerboseKey
"Pragma"
      A.Open         {} -> VerboseKey
"Open"
      A.FunDef       {} -> VerboseKey
"FunDef"
      A.DataSig      {} -> VerboseKey
"DataSig"
      A.DataDef      {} -> VerboseKey
"DataDef"
      A.RecSig       {} -> VerboseKey
"RecSig"
      A.RecDef       {} -> VerboseKey
"RecDef"
      A.PatternSynDef{} -> VerboseKey
"PatternSynDef"
      A.Generalize   {} -> VerboseKey
"Generalize"
      A.UnquoteDecl  {} -> VerboseKey
"UnquoteDecl"
      A.ScopedDecl   {} -> VerboseKey
"ScopedDecl"
      A.UnquoteDef   {} -> VerboseKey
"UnquoteDef"

debugPrintDecl :: A.Declaration -> TCM ()
debugPrintDecl :: Declaration -> TCM ()
debugPrintDecl Declaration
d = do
    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.decl" VerboseLevel
45 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
45 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checking a " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Declaration -> VerboseKey
forall a. ShowHead a => a -> VerboseKey
showHead Declaration
d
      case Declaration
d of
        A.Section Range
info ModuleName
mname GeneralizeTelescope
tel [Declaration]
ds -> do
          VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.decl" VerboseLevel
45 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
            VerboseKey
"section " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ModuleName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow ModuleName
mname VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" has "
              VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Telescope -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> VerboseLevel) -> Telescope -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ GeneralizeTelescope -> Telescope
A.generalizeTel GeneralizeTelescope
tel) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" parameters and "
              VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Declaration] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Declaration]
ds) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" declarations"
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Declaration -> TCM Doc) -> Declaration -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
info ModuleName
mname GeneralizeTelescope
tel []
          [Declaration] -> (Declaration -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Declaration]
ds ((Declaration -> TCM ()) -> TCM ())
-> (Declaration -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Declaration
d -> do
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.decl" VerboseLevel
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Declaration
d
        Declaration
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()