{-# 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.Map.Strict as MapS
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 <- 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)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache.decl" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"checkDeclCached: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (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 forall a. Eq a => a -> a -> Bool
== ModuleName
mname' Bool -> Bool -> Bool
&& Telescope
tbinds forall a. Eq a => a -> a -> Bool
== Telescope
tbinds' -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog forall a b. (a -> b) -> a -> b
$ ModuleName -> Telescope -> TypeCheckAction
EnterSection ModuleName
mname Telescope
tbinds
  Declaration -> TCM ()
checkDecl Declaration
d
  forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (LeaveSection ModuleName
mname', PostScopeState
_) | ModuleName
mname forall a. Eq a => a -> a -> Bool
== ModuleName
mname' -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog forall a b. (a -> b) -> a -> b
$ ModuleName -> TypeCheckAction
LeaveSection ModuleName
mname

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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache.decl" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"checkDeclCached: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (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
        forall (m :: * -> *).
(MonadDebug m, MonadTCState m) =>
PostScopeState -> m ()
restorePostScopeState PostScopeState
s
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache.decl" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"range: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (forall a. HasRange a => a -> Range
getRange Declaration
d)
        Range -> TCM ()
printSyntaxInfo (forall a. HasRange a => a -> Range
getRange Declaration
d)
      Maybe (TypeCheckAction, PostScopeState)
_ -> do
        forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
        Declaration -> TCM ()
checkDeclWrap Declaration
d
    forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog forall a b. (a -> b) -> a -> b
$ Declaration -> TypeCheckAction
Decl Declaration
d
 where
   compareDecl :: Declaration -> Declaration -> Bool
compareDecl A.Section{} A.Section{} = forall a. HasCallStack => a
__IMPOSSIBLE__
   compareDecl A.ScopedDecl{} A.ScopedDecl{} = forall a. HasCallStack => a
__IMPOSSIBLE__
   compareDecl Declaration
x Declaration
y = Declaration
x 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 = forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache forall a b. (a -> b) -> a -> b
$ do
     forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
     m a
m
   checkDeclWrap :: Declaration -> TCM ()
checkDeclWrap d :: Declaration
d@A.RecDef{} = forall {m :: * -> *} {a}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkDecl Declaration
d
   checkDeclWrap d :: Declaration
d@A.Mutual{} = forall {m :: * -> *} {a}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
45 forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Declaration]
ds) forall a. [a] -> [a] -> [a]
++ [Char]
" declarations..."
  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 = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Declaration
d forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking declaration"
    Declaration -> TCM ()
debugPrintDecl Declaration
d
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
90 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (Declaration -> [Declaration]
deepUnscopeDecl Declaration
d)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
10 forall a b. (a -> b) -> a -> b
$ 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 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  forall a. Maybe a
Nothing           -- skip all checks
        meta :: f a -> f (Maybe (m ()))
meta        f a
m = f a
m forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  forall a. a -> Maybe a
Just (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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  forall a. HasCallStack => a
__IMPOSSIBLE__
                        -- We're definitely inside a mutual block.

    (Maybe (TCM ())
finalChecks, LocalMetaStores
metas) <- forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy forall a b. (a -> b) -> a -> b
$ case Declaration
d of
      A.Axiom{}                -> forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta 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 -> forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode 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{}                -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
FieldOutsideRecord
      A.Primitive DefInfo
i QName
x Arg Expr
e        -> forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta 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 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    -> forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta 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 -> forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta 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       -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none forall a b. (a -> b) -> a -> b
$ ModuleInfo -> ModuleName -> TCM ()
checkImport ModuleInfo
i ModuleName
x
      A.Pragma Range
i Pragma
p             -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none forall a b. (a -> b) -> a -> b
$ Range -> Pragma -> TCM ()
checkPragma Range
i Pragma
p
      A.ScopedDecl ScopeInfo
scope [Declaration]
ds    -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none forall a b. (a -> b) -> a -> b
$ ScopeInfo -> TCM ()
setScope ScopeInfo
scope forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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  -> forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible forall a b. (a -> b) -> a -> b
$ 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 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   -> forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible forall a b. (a -> b) -> a -> b
$ 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 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 -> forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible forall a b. (a -> b) -> a -> b
$ 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 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.
                                    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.decl.mutual" Int
70 forall a b. (a -> b) -> a -> b
$ do
                                      Maybe MutualId
current <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
                                      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. a -> Maybe a
Just MutualId
blockId forall a. Eq a => a -> a -> Bool
== Maybe MutualId
current) forall a b. (a -> b) -> a -> b
$ do
                                        forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"" Int
0
                                          [ [Char]
"mutual block id discrepancy for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x
                                          , [Char]
"  current    mut. bl. = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Maybe MutualId
current
                                          , [Char]
"  calculated mut. bl. = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show MutualId
blockId
                                          ]

                                    forall (m :: * -> *) a. Monad m => a -> m a
return (MutualId
blockId, forall a. a -> Set a
Set.singleton QName
x)
      A.DataSig DefInfo
i QName
x GeneralizeTelescope
ps Expr
t       -> forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible 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        -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none 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{}                 -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
      A.PatternSynDef{}        -> forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is 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     -> forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is forall a b. (a -> b) -> a -> b
$ [DefInfo] -> [QName] -> Expr -> TCM ()
checkUnquoteDef [DefInfo]
is [QName]
xs Expr
e
      A.UnquoteData [DefInfo]
is QName
x UniverseCheck
uc [DefInfo]
js [QName]
cs Expr
e -> forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly ([DefInfo]
is forall a. [a] -> [a] -> [a]
++ [DefInfo]
js) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.data" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDecl data" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
        forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCM [QName]
unquoteTop (QName
xforall a. a -> [a] -> [a]
:[QName]
cs) Expr
e

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

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

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

      -- Post-typing checks.
      forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (TCM ())
finalChecks forall a b. (a -> b) -> a -> b
$ \ TCM ()
theMutualChecks -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Attempting to solve constraints before freezing."
        TCM ()
wakeupConstraints_   -- solve emptiness and instance constraints
        Bool
checkingWhere <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckingWhere
        DefaultToInfty -> TCM ()
solveSizeConstraints 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{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Declaration
_ -> do
              forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Freezing all open metas."
              forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTCState m =>
LocalMetaStore -> m (Set MetaId)
freezeMetas (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
metas)

        TCM ()
theMutualChecks

    where

    -- 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 :: 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 i
i m a
m = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
5 forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"Checking" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.abstract" Int
25 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. AnyIsAbstract a => a -> IsAbstract
anyIsAbstract i
i
      a
r <- forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly i
i m a
m
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
5 forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"Checked" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
      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 :: forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i) =>
i -> m a -> m a
checkMaybeAbstractly = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i o. Lens' i o -> LensSet i o
set forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. Set a -> [a]
Set.toList Set QName
names
  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.
  forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions (forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
SmallSet.delete AllowedReduction
UnconfirmedReductions) 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.
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = forall a. a -> Maybe a
Just MutualId
mid }) forall a b. (a -> b) -> a -> b
$
    Declaration -> TCM ()
checkTermination_ Declaration
d
  [QName] -> TCM ()
revisitRecordPatternTranslation [QName]
nameList -- Andreas, 2016-11-19 issue #2308

  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) <- forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *}.
HasConstInfo m =>
QName -> m (Maybe (Either QName (QName, CompiledClauses)))
classify [QName]
qs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [QName]
rs) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(QName, CompiledClauses)]
qccs forall a b. (a -> b) -> a -> b
$ \(QName
q,CompiledClauses
cc) -> do
    (CompiledClauses
cc, Bool
recordExpressionBecameCopatternLHS) <- forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateCompiledClauses forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just CompiledClauses
cc)
      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 = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q 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 } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left QName
q
      Function
        { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
MaybeProjection
            -- Andreas, 2017-08-10, issue #2664:
            -- Do not record pattern translate record projection definitions!
        , funCompiled :: Defn -> Maybe CompiledClauses
funCompiled   = Just CompiledClauses
cc
        } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (QName
q, CompiledClauses
cc)
      Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDecl" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
xs)
  forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCM [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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDef" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
xs)
  () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCM [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 -> TCM [QName]
unquoteTop [QName]
xs Expr
e = do
  Term
tcm   <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM
  Term
unit  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit
  Term
lzero <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero
  let vArg :: a -> Arg a
vArg = forall a. a -> Arg a
defaultArg
      hArg :: a -> Arg a
hArg = forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Arg a
vArg
  Term
m    <- forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
zeroQuantity forall a b. (a -> b) -> a -> b
$
            Expr -> Type -> TCMT IO Term
checkExpr Expr
e forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> [Arg Term] -> t
apply Term
tcm [forall a. a -> Arg a
hArg Term
lzero, forall a. a -> Arg a
vArg Term
unit]
  Either UnquoteError (Term, [QName])
res  <- forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName]
xs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Term
evalTCM Term
m
  case Either UnquoteError (Term, [QName])
res of
    Left UnquoteError
err      -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
    Right (Term
_, [QName]
xs) -> 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.inst" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"instantiating type of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
q
  Type
t  <- Definition -> Type
defType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Signature -> Maybe Definition
lookupDefinition QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  Type
t' <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Definition -> Definition
updateDefType forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Type
t'
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.inst" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"  t  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , TCMT IO Doc
"  t' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
45 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Highlighting a declaration with the following spine:"
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Declaration -> DeclarationSpine
A.declarationSpine Declaration
d)
  let highlight :: Declaration -> TCM ()
highlight Declaration
d = Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
d Level
Full Bool
True
  forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] forall a b. (a -> b) -> a -> b
$ case Declaration
d of
    A.Axiom{}                -> Declaration -> TCM ()
highlight Declaration
d
    A.Field{}                -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Primitive{}            -> Declaration -> TCM ()
highlight Declaration
d
    A.Mutual MutualInfo
i [Declaration]
ds            -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
DoHighlightModuleContents) 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{}           -> 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.UnquoteData{}           -> 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 [])
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HighlightModuleContents
hlmod forall a. Eq a => a -> a -> Bool
== HighlightModuleContents
DoHighlightModuleContents) forall a b. (a -> b) -> a -> b
$ 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
ps 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 forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString 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 = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Termination] forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking termination..."
  -- If there are some termination errors, we throw a warning.
  -- The termination checker already marked non-terminating functions as such.
  forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (Declaration -> TCM Result
termDecl Declaration
d) forall a b. (a -> b) -> a -> b
$ \ Result
termErrs -> do
    forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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 = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Positivity] forall a b. (a -> b) -> a -> b
$ do
  -- Positivity checking.
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"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.
  forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
 MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
 MonadDebug m, MonadPretty m) =>
[QName] -> m ()
computePolarity forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Declaration]
ds 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) <- forall a. RecordDirectives' a -> Maybe (Ranged Induction)
recInductive RecordDirectives
dir -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (QName -> TCMT IO Bool
isRecursiveRecord QName
q) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
      [Char]
"Only recursive records can be coinductive"
  Declaration
_ -> 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 = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Injectivity] forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ Set QName
names forall a b. (a -> b) -> a -> b
$ \ QName
q -> forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q 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 -> Either ProjectionLikenessMissing Projection
funProjection = Either ProjectionLikenessMissing Projection
mproj }
        | Maybe Bool
term forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Bool
True -> do
            -- Not terminating, thus, running the injectivity check could get us into a loop.
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Int
35 forall a b. (a -> b) -> a -> b
$
              forall a. Pretty a => a -> [Char]
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ [Char]
" is not verified as terminating, thus, not considered for injectivity"
        | Defn -> Bool
isProperProjection Defn
d -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Int
40 forall a b. (a -> b) -> a -> b
$
              forall a. Pretty a => a -> [Char]
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ [Char]
" is a projection, thus, not considered for injectivity"
        | Bool
otherwise -> do

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

      Defn
_ -> do
        AbstractMode
abstr <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Int
40 forall a b. (a -> b) -> a -> b
$
          [Char]
"we are in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show AbstractMode
abstr forall a. [a] -> [a] -> [a]
++ [Char]
" and " forall a. [a] -> [a] -> [a]
++
             forall a. Pretty a => a -> [Char]
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ [Char]
" 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 = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.ProjectionLikeness] forall a b. (a -> b) -> a -> b
$ do
      -- Non-mutual definitions can be considered for
      -- projection likeness
      let ds :: [QName]
ds = forall a. Set a -> [a]
Set.toList Set QName
names
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking projection-likeness of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [QName]
ds
      case [QName]
ds of
        [QName
d] -> do
          Definition
def <- 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
_          -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
25 forall a b. (a -> b) -> a -> b
$
              forall a. Pretty a => a -> [Char]
prettyShow QName
d forall a. [a] -> [a] -> [a]
++ [Char]
" is abstract or not a function, thus, not considered for projection-likeness"
        [QName]
_ -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
25 forall a b. (a -> b) -> a -> b
$
               [Char]
"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 :: forall a. 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 forall a. Eq a => a -> a -> Bool
/= IsAbstract
AbstractDef then TCM a
m else do
    (a
a, LocalMetaStores
ms) <- forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy TCM a
m
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Attempting to solve constraints before freezing."
    TCM ()
wakeupConstraints_   -- solve emptiness and instance constraints
    Set MetaId
xs <- forall (m :: * -> *).
MonadTCState m =>
LocalMetaStore -> m (Set MetaId)
freezeMetas (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
ms)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.ax" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"Abstract type signature produced new open metas: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
MapS.keys (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
ms))
      , TCMT IO Doc
"We froze the following ones of these:            " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set MetaId
xs)
      ]
    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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.gen" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking type signature of generalizable variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' DoGeneralize TCEnv
eGeneralizeMetas (forall a b. a -> b -> a
const DoGeneralize
YesGeneralizeMeta) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
    let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe QName]
telNames

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

    Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
    QName -> Definition -> TCM ()
addConstant QName
x 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 = Int -> NumGeneralizableArgs
SomeGeneralizableArgs Int
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' 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 = forall a. DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter DefInfo
i forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero 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 <- forall a. Ord a => a -> a -> a
max (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance
  Quantity
q   <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Quantity
getQuantity forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    q :: Quantity
q@Quantity0{} -> Quantity
q
    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 = 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 = forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info0
  forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c forall a b. (a -> b) -> a -> b
$ do

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

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

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

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Maybe Name]
genParams) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.ax" Int
40 forall a b. (a -> b) -> a -> b
$ [Char]
"  generalized params: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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!
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (KindOfName
kind forall a. Eq a => a -> a -> Bool
== KindOfName
AxiomName) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
t) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((forall a. Ord a => a -> a -> Bool
> Int
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"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   -> forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    Just [Occurrence]
occs -> do
      TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
      let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [Occurrence]
occs) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> Int -> TypeError
TooManyPolarities QName
x Int
n
      let pols :: [Polarity]
pols = forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc [Occurrence]
occs
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.pragma" Int
10 forall a b. (a -> b) -> a -> b
$
        [Char]
"Setting occurrences and polarity for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
":\n  " forall a. [a] -> [a] -> [a]
++
        forall a. Pretty a => a -> [Char]
prettyShow [Occurrence]
occs forall a. [a] -> [a] -> [a]
++ [Char]
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pols
      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   -> forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
x) ()
        KindOfName
MacroName -> forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
x) ()
        KindOfName
_         -> forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()

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

  Language
lang <- 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 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
fun
          KindOfName
MacroName -> forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro Bool
True Defn
fun
          KindOfName
DataName  -> Int -> Defn
DataOrRecSig Int
npars
          KindOfName
RecName   -> Int -> Defn
DataOrRecSig Int
npars
          KindOfName
AxiomName -> Defn
defaultAxiom     -- Old comment: NB: used also for data and record type sigs
          KindOfName
_         -> forall a. HasCallStack => a
__IMPOSSIBLE__
        where fun :: Defn
fun = FunctionData -> Defn
FunctionDefn forall a b. (a -> b) -> a -> b
$ FunctionData
emptyFunctionData{ _funAbstr :: IsAbstract
_funAbstr = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i }

  QName -> Definition -> TCM ()
addConstant QName
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    Definition -> TCMT IO Definition
useTerPragma 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 forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
    InstanceDef Range
_r -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
IsType_ Expr
e) 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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckingWhere
    DefaultToInfty -> TCM ()
solveSizeConstraints 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) =
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Expr -> Call
CheckPrimitive (forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
x Expr
e) forall a b. (a -> b) -> a -> b
$ do
    ([Char]
name, PrimImpl Type
t' PrimFun
pf) <- QName -> TCM ([Char], PrimitiveImpl)
lookupPrimitiveFunctionQ QName
x
    -- Certain "primitive" functions are BUILTIN rather than
    -- primitive.
    let builtinPrimitives :: [[Char]]
builtinPrimitives =
          [ [Char]
"primNatPlus"
          , [Char]
"primNatMinus"
          , [Char]
"primNatTimes"
          , [Char]
"primNatDivSucAux"
          , [Char]
"primNatModSucAux"
          , [Char]
"primNatEquality"
          , [Char]
"primNatLess"
          , [Char]
"primLevelZero"
          , [Char]
"primLevelSuc"
          , [Char]
"primLevelMax"
          , [Char]
"primSetOmega"
          , [Char]
"primStrictSet"
          , [Char]
"primStrictSetOmega"
          ]
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
builtinPrimitives) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.prim" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
name forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is a BUILTIN, not a primitive!"
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
NoSuchPrimitiveFunction [Char]
name
    Type
t <- Expr -> TCMT IO Type
isType_ Expr
e
    forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t Type
t'
    let s :: [Char]
s  = forall a. Pretty a => a -> [Char]
prettyShow 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 [Char]
name of
            -- Currently no special primitives
            [Char]
_ -> ArgInfo
defaultArgInfo
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ArgInfo
info forall a. Eq a => a -> a -> Bool
== ArgInfo
expectedInfo) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> ArgInfo -> ArgInfo -> TypeError
WrongModalityForPrimitive [Char]
name ArgInfo
info ArgInfo
expectedInfo
    [Char] -> PrimFun -> TCM ()
bindPrimitive [Char]
s PrimFun
pf
    QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
x ArgInfo
info QName
x Type
t forall a b. (a -> b) -> a -> b
$
        Primitive { primAbstr :: IsAbstract
primAbstr    = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
                  , primName :: [Char]
primName     = [Char]
s
                  , primClauses :: [Clause]
primClauses  = []
                  , primInv :: FunctionInverse
primInv      = forall c. FunctionInverse' c
NotInjective
                  , primCompiled :: Maybe CompiledClauses
primCompiled = forall a. Maybe a
Nothing }

-- | Check a pragma.
checkPragma :: Range -> A.Pragma -> TCM ()
checkPragma :: Range -> Pragma -> TCM ()
checkPragma Range
r Pragma
p =
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> Pragma -> Call
CheckPragma Range
r Pragma
p) forall a b. (a -> b) -> a -> b
$ case Pragma
p of
        A.BuiltinPragma RString
rb ResolvedName
x
          | [Char] -> Bool
isUntypedBuiltin [Char]
b -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          | Bool
otherwise          -> [Char] -> ResolvedName -> TCM ()
bindBuiltin [Char]
b ResolvedName
x
          where b :: [Char]
b = forall a. Ranged a -> a
rangedThing RString
rb
        A.BuiltinNoDefPragma RString
b KindOfName
_kind QName
x -> [Char] -> QName -> TCM ()
bindBuiltinNoDef (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 [Char]
s -> do
          -- Check that x resides in the same module (or a child) as the pragma.
          QName
x' <- Definition -> QName
defName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x  -- Get the canonical name of x.
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((QName
x' QName -> ModuleName -> Bool
`isInModule`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
              [Char]
"COMPILE pragmas must appear in the same module as their corresponding definitions,"
          [Char] -> QName -> [Char] -> TCM ()
addPragma (forall a. Ranged a -> a
rangedThing RString
b) QName
x [Char]
s
        A.StaticPragma QName
x -> do
          Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          case Definition -> Defn
theDef Definition
def of
            Function{} -> QName -> TCM ()
markStatic QName
x
            Defn
_          -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"STATIC directive only works on functions"
        A.InjectivePragma QName
x -> QName -> TCM ()
markInjective QName
x
        A.NotProjectionLikePragma QName
qn -> do
          Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
          case Definition -> Defn
theDef Definition
def of
            it :: Defn
it@Function{} ->
              forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
qn forall a b. (a -> b) -> a -> b
$ \Definition
def -> Definition
def { theDef :: Defn
theDef = Defn
it { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = forall a b. a -> Either a b
Left ProjectionLikenessMissing
NeverProjection } }
            Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"NOT_PROJECTION_LIKE directive only applies to functions"
        A.InlinePragma Bool
b QName
x -> do
          Definition
def <- 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
_          -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
sINLINE forall a. [a] -> [a] -> [a]
++ [Char]
" directive only works on functions"
              where sINLINE :: [Char]
sINLINE = if Bool
b then [Char]
"INLINE" else [Char]
"NOINLINE"
        A.OptionsPragma{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
                [Char]
"ETA pragma is only applicable to coinductive records"
          forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) forall {a}. TCMT IO a
noRecord forall a b. (a -> b) -> a -> b
$ \case
            Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality
eta } -> do
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe Induction
ind forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Induction
CoInductive) forall a b. (a -> b) -> a -> b
$ forall {a}. TCMT IO a
noRecord
              if | Specified NoEta{} <- EtaEquality
eta -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
                     [Char]
"ETA pragma conflicts with no-eta-equality declaration"
                 | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
r forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
            def :: Defn
def@Record{} -> Defn
def { recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta' PatternOrCopattern -> EtaEquality
Specified forall a. HasEta' a
YesEta }
            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 = forall a. (MutualId -> TCM a) -> TCM a
inMutualBlock forall a b. (a -> b) -> a -> b
$ \ MutualId
blockId -> forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero forall a b. (a -> b) -> a -> b
$ do

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

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

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

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


-- | Type check the type signature of an inductive or recursive definition.
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature :: Declaration -> TCM ()
checkTypeSignature = Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' 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
  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) =
  forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.TypeSig] forall a b. (a -> b) -> a -> b
$
    let abstr :: TCM () -> TCM ()
abstr = case forall t. DefInfo' t -> Access
Info.defAccess DefInfo
i of
          PrivateAccess{}
            | forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef -> 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 -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
          Access
PublicAccess  -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    in TCM () -> TCM ()
abstr 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
_ =
  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 = forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection ModuleName
x GeneralizeTelescope
tel forall a b. (a -> b) -> a -> b
$ 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
-> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
checkModuleArity ModuleName
m Tele (Dom Type)
tel [NamedArg Expr]
args = Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
  where
    bad :: TCM (Tele (Dom Type))
bad = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ModuleName -> Tele (Dom Type) -> [NamedArg Expr] -> TypeError
ModuleArityMismatch ModuleName
m Tele (Dom Type)
tel [NamedArg Expr]
args

    check :: Telescope -> [NamedArg A.Expr] -> TCM Telescope
    check :: Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel []             = forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom Type)
tel
    check Tele (Dom Type)
EmptyTel (NamedArg Expr
_:[NamedArg Expr]
_)     = TCM (Tele (Dom Type))
bad
    check (ExtendTel dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} Abs (Tele (Dom Type))
btel) args0 :: [NamedArg Expr]
args0@(Arg ArgInfo
info' Named_ Expr
arg : [NamedArg Expr]
args) =
      let name :: Maybe [Char]
name = forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
bareNameOf Named_ Expr
arg
          my :: Maybe [Char]
my   = forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
bareNameOf Dom Type
dom
          tel :: Tele (Dom Type)
tel  = forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom Type))
btel in
      case (ArgInfo -> Hiding
argInfoHiding ArgInfo
info, ArgInfo -> Hiding
argInfoHiding ArgInfo
info', Maybe [Char]
name) of
        (Instance{}, Hiding
NotHidden, Maybe [Char]
_)        -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Instance{}, Hiding
Hidden, Maybe [Char]
_)           -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Instance{}, Instance{}, Maybe [Char]
Nothing) -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
        (Instance{}, Instance{}, Just [Char]
x)
          | forall a. a -> Maybe a
Just [Char]
x forall a. Eq a => a -> a -> Bool
== Maybe [Char]
my                  -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Hiding
NotHidden, Maybe [Char]
_)            -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Instance{}, Maybe [Char]
_)           -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Hiding
Hidden, Hiding
Hidden, Maybe [Char]
Nothing)         -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
        (Hiding
Hidden, Hiding
Hidden, Just [Char]
x)
          | forall a. a -> Maybe a
Just [Char]
x forall a. Eq a => a -> a -> Bool
== Maybe [Char]
my                  -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args0
        (Hiding
NotHidden, Hiding
NotHidden, Maybe [Char]
_)         -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
check Tele (Dom Type)
tel [NamedArg Expr]
args
        (Hiding
NotHidden, Hiding
Hidden, Maybe [Char]
_)            -> TCM (Tele (Dom Type))
bad
        (Hiding
NotHidden, Instance{}, Maybe [Char]
_)        -> TCM (Tele (Dom Type))
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 =
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> ModuleName -> ModuleApplication -> Call
CheckSectionApplication (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) ModuleName
m1 ModuleApplication
modapp) forall a b. (a -> b) -> a -> b
$
  -- A section application is type-checked in a non-erased context
  -- (#5410).
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall i o. Lens' i o -> LensMap i o
over Lens' Quantity TCEnv
eQuantity forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
`addQuantity` Quantity
topQuantity)) 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.
  Int
extraParams <- do
    Int
mfv <- TCMT IO Int
getCurrentModuleFreeVars
    Int
fv  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
    forall (m :: * -> *) a. Monad m => a -> m a
return (Int
fv forall a. Num a => a -> a -> a
- Int
mfv)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
extraParams forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.mod.apply" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"Extra parameters to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m1 forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
extraParams
  -- Type-check the LHS (ptel) of the module macro.
  forall a. Telescope -> (Tele (Dom Type) -> TCM a) -> TCM a
checkTelescope Telescope
ptel forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
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)`.
    Tele (Dom Type)
tel <- forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m2
    [Arg Term]
vs  <- forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply ModuleName
m2
    let tel' :: Tele (Dom Type)
tel'  = forall t. Apply t => t -> [Arg Term] -> t
apply Tele (Dom Type)
tel [Arg Term]
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.
    Tele (Dom Type)
etaTel <- ModuleName
-> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
checkModuleArity ModuleName
m2 Tele (Dom Type)
tel' [NamedArg Expr]
args
    -- Take the module parameters that will be instantiated by @args@.
    let tel'' :: Tele (Dom Type)
tel'' = ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall a. Sized a => a -> Int
size Tele (Dom Type)
tel' forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Tele (Dom Type)
etaTel) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel'
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"applying section" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m2
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Expr]
args)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ptel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Int
size Tele (Dom Type)
ptel) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
ptel)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel'
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel''=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel''
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"eta  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Int
size Tele (Dom Type)
ptel) (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel'' forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
etaTel)
      ]
    -- Now, type check arguments.
    [Arg Term]
ts <- forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Tele (Dom Type)
-> TCM (Elims, Tele (Dom Type))
checkArguments_ Comparison
CmpEq ExpandHidden
DontExpandLast (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) [NamedArg Expr]
args Tele (Dom Type)
tel') forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (Elims
ts', Tele (Dom Type)
etaTel') | (forall a. Sized a => a -> Int
size Tele (Dom Type)
etaTel forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Tele (Dom Type)
etaTel')
                     , Just [Arg Term]
ts <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
ts' -> forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
ts
      (Elims, Tele (Dom Type))
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Perform the application of the module parameters.
    let aTel :: Tele (Dom Type)
aTel = Tele (Dom Type)
tel' forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"aTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
aTel
      ]
    -- Andreas, 2014-04-06, Issue 1094:
    -- Add the section with well-formed telescope.
    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. a -> KeepNames a
KeepNames Tele (Dom Type)
aTel) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
80 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"addSection" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m1 forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Tele (Dom Type)
tel -> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel))
      ModuleName -> TCM ()
addSection ModuleName
m1

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

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

      telInst :: Telescope
      telInst :: Tele (Dom Type)
telInst = Tele (Dom Type) -> Tele (Dom Type)
instFinal Tele (Dom Type)
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 :: Tele (Dom Type) -> Tele (Dom Type)
instFinal (ExtendTel Dom Type
_ NoAbs{}) = forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Found last parameter: switch it to @Instance@.
      instFinal (ExtendTel Dom Type
dom (Abs [Char]
n Tele (Dom Type)
EmptyTel)) =
                 forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
do' (forall a. [Char] -> a -> Abs a
Abs [Char]
n forall a. Tele a
EmptyTel)
        where do' :: Dom Type
do' = forall a. LensHiding a => a -> a
makeInstance Dom Type
dom { domName :: Maybe NamedName
domName = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged [Char]
"r" }
      -- Otherwise, keep searchinf for last parameter:
      instFinal (ExtendTel Dom Type
arg (Abs [Char]
n Tele (Dom Type)
tel)) =
                 forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
arg (forall a. [Char] -> a -> Abs a
Abs [Char]
n (Tele (Dom Type) -> Tele (Dom Type)
instFinal Tele (Dom Type)
tel))
      -- Before instFinal is invoked, we have checked that the @tel@ is not empty.
      instFinal Tele (Dom Type)
EmptyTel = forall a. HasCallStack => a
__IMPOSSIBLE__

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

  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
telInst forall a b. (a -> b) -> a -> b
$ do
    [Arg Term]
vs <- forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply ModuleName
x
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) [Arg Term]
args)
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.mod.apply" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show [Arg Term]
vs)
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show [Arg Term]
args)
      ]
    ModuleName -> TCM ()
addSection ModuleName
m1
    ModuleName
-> Tele (Dom Type)
-> ModuleName
-> [Arg Term]
-> ScopeCopyInfo
-> TCM ()
applySection ModuleName
m1 Tele (Dom Type)
telInst ModuleName
x ([Arg Term]
vs forall a. [a] -> [a] -> [a]
++ [Arg Term]
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 = forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

class ShowHead a where
  showHead :: a -> String

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

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