{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Def where

import Prelude hiding ( mapM, null )

import Control.Arrow (first,second)
import Control.Monad.State hiding (forM, mapM)

import Data.Function
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Traversable (forM, mapM)
import Data.Semigroup (Semigroup((<>)))
import Data.Tuple ( swap )

import Agda.Interaction.Options

import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Pattern as A
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Fixity
import Agda.Syntax.Info

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Warnings ( warning )

import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Inlining
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.CompiledClause (CompiledClauses'(..), hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)

import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.LHS                 ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )

import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Definitions by pattern matching
---------------------------------------------------------------------------

checkFunDef :: Delayed -> A.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef Delayed
delayed DefInfo
i QName
name [Clause]
cs = do
        -- Reset blocking tag (in case a previous attempt was blocked)
        (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
-> (Blocked_ -> Blocked_) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Blocked_ -> Blocked_
forall a b. a -> b -> a
const (Blocked_ -> Blocked_ -> Blocked_)
-> Blocked_ -> Blocked_ -> Blocked_
forall a b. (a -> b) -> a -> b
$
          NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
MissingClauses ()
        -- Get the type and relevance of the function
        Definition
def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
        let t :: Type
t    = Definition -> Type
defType Definition
def
        let info :: ArgInfo
info = Definition -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Definition
def
        case [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause]
cs Type
t of
          Just (Expr
e, Maybe Expr
mc, MetaId
x) ->
            Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> QName -> [Clause] -> Call
CheckFunDefCall (DefInfo -> Range
forall t. HasRange t => t -> Range
getRange DefInfo
i) QName
name [Clause]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
              -- Andreas, 2012-11-22: if the alias is in an abstract block
              -- it has been frozen.  We unfreeze it to enable type inference.
              -- See issue 729.
              TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
              Type
-> ArgInfo
-> Delayed
-> DefInfo
-> QName
-> Expr
-> Maybe Expr
-> TCM ()
checkAlias Type
t ArgInfo
info Delayed
delayed DefInfo
i QName
name Expr
e Maybe Expr
mc
          Maybe (Expr, Maybe Expr, MetaId)
_ -> Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Delayed
delayed Maybe ExtLamInfo
forall a. Maybe a
Nothing Maybe QName
forall a. Maybe a
Nothing DefInfo
i QName
name [Clause]
cs

        -- If it's a macro check that it ends in Term → TC ⊤
        let ismacro :: Bool
ismacro = Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> Definition -> Bool
forall a b. (a -> b) -> a -> b
$ Definition
def
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
ismacro Bool -> Bool -> Bool
|| DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM ()
checkMacroType Type
t
    TCM () -> ((TCErr, MetaId) -> TCM ()) -> TCM ()
forall a. TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, MetaId
x) -> do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          [ TCM Doc
"checking function definition got stuck on meta: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (MetaId -> VerboseKey
forall a. Show a => a -> VerboseKey
show MetaId
x) ]
        (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
-> (Blocked_ -> Blocked_) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Blocked_ -> Blocked_
forall a b. a -> b -> a
const (Blocked_ -> Blocked_ -> Blocked_)
-> Blocked_ -> Blocked_ -> Blocked_
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x ()
        Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Delayed -> DefInfo -> QName -> [Clause] -> Constraint
CheckFunDef Delayed
delayed DefInfo
i QName
name [Clause]
cs

checkMacroType :: Type -> TCM ()
checkMacroType :: Type -> TCM ()
checkMacroType Type
t = do
  Type
t' <- Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
t
  TelV Tele (Dom Type)
tel Type
tr <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t'

  let telList :: [Dom (VerboseKey, Type)]
telList = Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
      resType :: Type
resType = Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract ([Dom (VerboseKey, Type)] -> Tele (Dom Type)
telFromList (VerboseLevel
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. VerboseLevel -> [a] -> [a]
drop ([Dom (VerboseKey, Type)] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Dom (VerboseKey, Type)]
telList VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) [Dom (VerboseKey, Type)]
telList)) Type
tr
  Type
expectedType <- TCMT IO Term -> TCMT IO Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCMT IO Type -> TCMT IO Type -> TCMT IO Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCMT IO Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
resType Type
expectedType
    TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"Result type of a macro must be"
                                                            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
expectedType ]

-- | A single clause without arguments and without type signature is an alias.
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause]
cs Type
t =
        case [Clause] -> Maybe (Expr, Maybe Expr)
trivialClause [Clause]
cs of
          -- if we have just one clause without pattern matching and
          -- without a type signature, then infer, to allow
          -- "aliases" for things starting with hidden abstractions
          Just (Expr
e, Maybe Expr
mc) | Just MetaId
x <- Term -> Maybe MetaId
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) -> (Expr, Maybe Expr, MetaId) -> Maybe (Expr, Maybe Expr, MetaId)
forall a. a -> Maybe a
Just (Expr
e, Maybe Expr
mc, MetaId
x)
          Maybe (Expr, Maybe Expr)
_ -> Maybe (Expr, Maybe Expr, MetaId)
forall a. Maybe a
Nothing
  where
    isMeta :: Term -> Maybe MetaId
isMeta (MetaV MetaId
x Elims
_) = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x
    isMeta Term
_           = Maybe MetaId
forall a. Maybe a
Nothing
    trivialClause :: [Clause] -> Maybe (Expr, Maybe Expr)
trivialClause [A.Clause (A.LHS LHSInfo
i (A.LHSHead QName
f [])) [ProblemEq]
_ (A.RHS Expr
e Maybe Expr
mc) (A.WhereDecls Maybe ModuleName
_ []) Bool
_] = (Expr, Maybe Expr) -> Maybe (Expr, Maybe Expr)
forall a. a -> Maybe a
Just (Expr
e, Maybe Expr
mc)
    trivialClause [Clause]
_ = Maybe (Expr, Maybe Expr)
forall a. Maybe a
Nothing

-- | Check a trivial definition of the form @f = e@
checkAlias :: Type -> ArgInfo -> Delayed -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias :: Type
-> ArgInfo
-> Delayed
-> DefInfo
-> QName
-> Expr
-> Maybe Expr
-> TCM ()
checkAlias Type
t ArgInfo
ai Delayed
delayed DefInfo
i QName
name Expr
e Maybe Expr
mc =
  let clause :: Clause' SpineLHS
clause = Clause :: forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause { clauseLHS :: SpineLHS
clauseLHS          = LHSInfo -> QName -> [NamedArg (Pattern' Expr)] -> SpineLHS
A.SpineLHS (Range -> ExpandedEllipsis -> LHSInfo
LHSInfo (DefInfo -> Range
forall t. HasRange t => t -> Range
getRange DefInfo
i) ExpandedEllipsis
NoEllipsis) QName
name []
                        , clauseStrippedPats :: [ProblemEq]
clauseStrippedPats = []
                        , clauseRHS :: RHS
clauseRHS          = Expr -> Maybe Expr -> RHS
A.RHS Expr
e Maybe Expr
mc
                        , clauseWhereDecls :: WhereDeclarations
clauseWhereDecls   = WhereDeclarations
A.noWhereDecls
                        , clauseCatchall :: Bool
clauseCatchall     = Bool
False } in
  QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCM ()
-> TCM ()
forall a.
QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCM a
-> TCM a
atClause QName
name VerboseLevel
0 Type
t Maybe Substitution
forall a. Maybe a
Nothing Clause' SpineLHS
clause (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.alias" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checkAlias" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
name) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
forall (m :: * -> *). Monad m => m Doc
colon  TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
name) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
forall (m :: * -> *). Monad m => m Doc
equals TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
    ]

  -- Infer the type of the rhs.
  -- Andreas, 2018-06-09, issue #2170.
  -- The context will only be resurrected if we have --irrelevant-projections.
  Term
v <- ArgInfo -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCMT IO Term
checkDontExpandLast Comparison
CmpLeq Expr
e Type
t

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.alias" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checkAlias: finished checking"

  DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty

  Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v  -- if we omit this, we loop (stdlib: Relation.Binary.Sum)
    -- or the termination checker might stumble over levels in sorts
    -- that cannot be converted to expressions without the level built-ins
    -- (test/succeed/Issue655.agda)

  -- compute body modification for irrelevant definitions, see issue 610
  let bodyMod :: Term -> Term
bodyMod = case ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai of
        Relevance
Irrelevant -> Term -> Term
dontCare
        Relevance
_          -> Term -> Term
forall a. a -> a
id

  -- Add the definition
  QName -> Definition -> TCM ()
addConstant QName
name (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
ai QName
name Type
t
                   (Defn -> Definition) -> Defn -> Definition
forall a b. (a -> b) -> a -> b
$ Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro (DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
                     Defn
emptyFunction
                      { funClauses :: [Clause]
funClauses = [ Clause :: Range
-> Range
-> Tele (Dom Type)
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause  -- trivial clause @name = v@
                          { clauseLHSRange :: Range
clauseLHSRange  = DefInfo -> Range
forall t. HasRange t => t -> Range
getRange DefInfo
i
                          , clauseFullRange :: Range
clauseFullRange = DefInfo -> Range
forall t. HasRange t => t -> Range
getRange DefInfo
i
                          , clauseTel :: Tele (Dom Type)
clauseTel       = Tele (Dom Type)
forall a. Tele a
EmptyTel
                          , namedClausePats :: NAPs
namedClausePats = []
                          , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
bodyMod Term
v
                          , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Type -> Arg Type
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Type
t
                          , clauseCatchall :: Bool
clauseCatchall  = Bool
False
                          , clauseRecursive :: Maybe Bool
clauseRecursive = Maybe Bool
forall a. Maybe a
Nothing   -- we don't know yet
                          , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                          , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
                          } ]
                      , funCompiled :: Maybe CompiledClauses
funCompiled = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just (CompiledClauses -> Maybe CompiledClauses)
-> CompiledClauses -> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ [Arg VerboseKey] -> Term -> CompiledClauses
forall a. [Arg VerboseKey] -> a -> CompiledClauses' a
Done [] (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Term -> Term
bodyMod Term
v
                      , funSplitTree :: Maybe SplitTree
funSplitTree = SplitTree -> Maybe SplitTree
forall a. a -> Maybe a
Just (SplitTree -> Maybe SplitTree) -> SplitTree -> Maybe SplitTree
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> SplitTree
forall a. VerboseLevel -> SplitTree' a
SplittingDone VerboseLevel
0
                      , funDelayed :: Delayed
funDelayed  = Delayed
delayed
                      , funAbstr :: IsAbstract
funAbstr    = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
                      }

  -- Andreas, 2017-01-01, issue #2372:
  -- Add the definition to the instance table, if needed, to update its type.
  case DefInfo -> IsInstance
forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
    InstanceDef Range
_r -> QName -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange QName
name (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCM ()
addTypedInstance QName
name Type
t
      -- Put highlighting on the name only;
      -- @(getRange (r, name))@ does not give good results.
    IsInstance
NotInstanceDef -> () -> TCM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.alias" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checkAlias: leaving"


-- | Type check a definition by pattern matching.
checkFunDef' :: Type             -- ^ the type we expect the function to have
             -> ArgInfo          -- ^ is it irrelevant (for instance)
             -> Delayed          -- ^ are the clauses delayed (not unfolded willy-nilly)
             -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
                                 --   (if so, we need to know some stuff about lambda-lifted args)
             -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
             -> A.DefInfo        -- ^ range info
             -> QName            -- ^ the name of the function
             -> [A.Clause]       -- ^ the clauses to check
             -> TCM ()
checkFunDef' :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type
t ArgInfo
ai Delayed
delayed Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name [Clause]
cs =
  Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe Substitution
-> [Clause]
-> TCM ()
checkFunDefS Type
t ArgInfo
ai Delayed
delayed Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name Maybe Substitution
forall a. Maybe a
Nothing [Clause]
cs

-- | Type check a definition by pattern matching.
checkFunDefS :: Type             -- ^ the type we expect the function to have
             -> ArgInfo          -- ^ is it irrelevant (for instance)
             -> Delayed          -- ^ are the clauses delayed (not unfolded willy-nilly)
             -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
                                 --   (if so, we need to know some stuff about lambda-lifted args)
             -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
             -> A.DefInfo        -- ^ range info
             -> QName            -- ^ the name of the function
             -> Maybe Substitution -- ^ substitution (from with abstraction) that needs to be applied to module parameters
             -> [A.Clause]       -- ^ the clauses to check
             -> TCM ()
checkFunDefS :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe Substitution
-> [Clause]
-> TCM ()
checkFunDefS Type
t ArgInfo
ai Delayed
delayed Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name Maybe Substitution
withSub [Clause]
cs = do

    Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> QName -> [Clause] -> Call
CheckFunDefCall (DefInfo -> Range
forall t. HasRange t => t -> Range
getRange DefInfo
i) QName
name [Clause]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.fun" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"checking body of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"full type:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> TCM Doc) -> (Definition -> Type) -> Definition -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCM Doc) -> TCMT IO Definition -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name)
              ]

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.fun" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [ TCM Doc
"clauses:" ] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> (Clause -> TCM Doc) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Clause -> VerboseKey) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Clause -> VerboseKey)
-> (Clause -> Clause) -> Clause -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Clause
forall a. ExprLike a => a -> a
A.deepUnscope) [Clause]
cs

        [Clause' SpineLHS]
cs <- [Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS])
-> [Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS]
forall a b. (a -> b) -> a -> b
$ (Clause -> Clause' SpineLHS) -> [Clause] -> [Clause' SpineLHS]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Clause' SpineLHS
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine [Clause]
cs

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.fun" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [ TCM Doc
"spine clauses:" ] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ (Clause' SpineLHS -> TCM Doc) -> [Clause' SpineLHS] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc)
-> (Clause' SpineLHS -> TCM Doc) -> Clause' SpineLHS -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Clause' SpineLHS -> VerboseKey) -> Clause' SpineLHS -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' SpineLHS -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Clause' SpineLHS -> VerboseKey)
-> (Clause' SpineLHS -> Clause' SpineLHS)
-> Clause' SpineLHS
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' SpineLHS -> Clause' SpineLHS
forall a. ExprLike a => a -> a
A.deepUnscope) [Clause' SpineLHS]
cs

        -- Ensure that all clauses have the same number of trailing hidden patterns
        -- This is necessary since trailing implicits are no longer eagerly inserted.
        -- Andreas, 2013-10-13
        -- Since we have flexible function arity, it is no longer necessary
        -- to patch clauses to same arity
        -- cs <- trailingImplicits t cs

        -- Check the clauses
        [(Clause, ClausesPostChecks)]
cs <- Call
-> TCMT IO [(Clause, ClausesPostChecks)]
-> TCMT IO [(Clause, ClausesPostChecks)]
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall Call
NoHighlighting (TCMT IO [(Clause, ClausesPostChecks)]
 -> TCMT IO [(Clause, ClausesPostChecks)])
-> TCMT IO [(Clause, ClausesPostChecks)]
-> TCMT IO [(Clause, ClausesPostChecks)]
forall a b. (a -> b) -> a -> b
$ do -- To avoid flicker.
          [(Clause' SpineLHS, VerboseLevel)]
-> ((Clause' SpineLHS, VerboseLevel)
    -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO [(Clause, ClausesPostChecks)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Clause' SpineLHS]
-> [VerboseLevel] -> [(Clause' SpineLHS, VerboseLevel)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Clause' SpineLHS]
cs [VerboseLevel
0..]) (((Clause' SpineLHS, VerboseLevel)
  -> TCMT IO (Clause, ClausesPostChecks))
 -> TCMT IO [(Clause, ClausesPostChecks)])
-> ((Clause' SpineLHS, VerboseLevel)
    -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO [(Clause, ClausesPostChecks)]
forall a b. (a -> b) -> a -> b
$ \ (Clause' SpineLHS
c, VerboseLevel
clauseNo) -> do
            QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCM a
-> TCM a
atClause QName
name VerboseLevel
clauseNo Type
t Maybe Substitution
withSub Clause' SpineLHS
c (TCMT IO (Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
              (Clause
c,ClausesPostChecks
b) <- ArgInfo
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO (Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
                Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe Substitution
withSub Clause' SpineLHS
c
              -- Andreas, 2013-11-23 do not solve size constraints here yet
              -- in case we are checking the body of an extended lambda.
              -- 2014-04-24: The size solver requires each clause to be
              -- checked individually, since otherwise we get constraints
              -- in typing contexts which are not prefixes of each other.
              Maybe ExtLamInfo -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> m () -> m ()
whenNothing Maybe ExtLamInfo
extlam (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty
              -- Andreas, 2013-10-27 add clause as soon it is type-checked
              -- TODO: instantiateFull?
              TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> TCM ()
addClauses QName
name [Clause
c]
              (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
c,ClausesPostChecks
b)

        ([Clause]
cs, CPC IntSet
isOneIxs) <- ([Clause], ClausesPostChecks)
-> TCMT IO ([Clause], ClausesPostChecks)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Clause], ClausesPostChecks)
 -> TCMT IO ([Clause], ClausesPostChecks))
-> ([Clause], ClausesPostChecks)
-> TCMT IO ([Clause], ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ (([ClausesPostChecks] -> ClausesPostChecks)
-> ([Clause], [ClausesPostChecks]) -> ([Clause], ClausesPostChecks)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [ClausesPostChecks] -> ClausesPostChecks
forall a. Monoid a => [a] -> a
mconcat (([Clause], [ClausesPostChecks]) -> ([Clause], ClausesPostChecks))
-> ([(Clause, ClausesPostChecks)]
    -> ([Clause], [ClausesPostChecks]))
-> [(Clause, ClausesPostChecks)]
-> ([Clause], ClausesPostChecks)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Clause, ClausesPostChecks)] -> ([Clause], [ClausesPostChecks])
forall a b. [(a, b)] -> ([a], [b])
unzip) [(Clause, ClausesPostChecks)]
cs

        let isSystem :: Bool
isSystem = Bool -> Bool
not (Bool -> Bool) -> (IntSet -> Bool) -> IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
forall a. Null a => a -> Bool
null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet
isOneIxs

        Bool
canBeSystem <- do
          -- allow VarP and ConP i0/i1 fallThrough = yes, DotP
          let pss :: [NAPs]
pss = (Clause -> NAPs) -> [Clause] -> [NAPs]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> NAPs
namedClausePats [Clause]
cs
              allowed :: Pattern' x -> Bool
allowed Pattern' x
p = case Pattern' x
p of
                VarP{} -> Bool
True
                -- pattern inserted by splitPartial
                ConP ConHead
_ ConPatternInfo
cpi [] | ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
cpi -> Bool
True
                DotP{} -> Bool
True
                Pattern' x
_      -> Bool
False
          Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$! (NamedArg (Pattern' DBPatVar) -> Bool) -> NAPs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' DBPatVar -> Bool
forall x. Pattern' x -> Bool
allowed (Pattern' DBPatVar -> Bool)
-> (NamedArg (Pattern' DBPatVar) -> Pattern' DBPatVar)
-> NamedArg (Pattern' DBPatVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' DBPatVar) -> Pattern' DBPatVar
forall a. NamedArg a -> a
namedArg) ([NAPs] -> NAPs
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [NAPs]
pss)
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
canBeSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError VerboseKey
"no pattern matching or path copatterns in systems!"


        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.fun" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [ TCM Doc
"checked clauses:" ] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> (Clause -> TCM Doc) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Clause -> VerboseKey) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [Clause]
cs

        -- After checking, remove the clauses again.
        -- (Otherwise, @checkInjectivity@ loops for issue 801).
        QName -> ([Clause] -> [Clause]) -> TCM ()
modifyFunClauses QName
name ([Clause] -> [Clause] -> [Clause]
forall a b. a -> b -> a
const [])

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"clauses before injectivity test"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [QNamed Clause] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([QNamed Clause] -> TCM Doc) -> [QNamed Clause] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> QNamed Clause) -> [Clause] -> [QNamed Clause]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs  -- broken, reify (QNamed n cl) expect cl to live at top level
              ]
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"raw clauses: "
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Clause -> VerboseKey) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QNamed Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show (QNamed Clause -> VerboseKey)
-> (Clause -> QNamed Clause) -> Clause -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs
              ]

        -- Needed to calculate the proper fullType below.
        -- Also: issue #4173, allow splitting on erased arguments in erased definitions
        -- in the coverage checker.
        ArgInfo -> TCM () -> TCM ()
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext ArgInfo
ai (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TCM () -> TCM ()
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        -- Systems have their own coverage and "coherence" check, we
        -- also add an absurd clause for the cases not needed.
        ([Clause]
cs,Maybe System
sys) <- if Bool -> Bool
not Bool
isSystem then ([Clause], Maybe System) -> TCMT IO ([Clause], Maybe System)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
cs, Maybe System
forall a. Null a => a
empty) else do
                 Type
fullType <- (Tele (Dom Type) -> Type -> Type)
-> Type -> Tele (Dom Type) -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Type
t (Tele (Dom Type) -> Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
                 System
sys <- TCMT IO System -> TCMT IO System
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO System -> TCMT IO System)
-> TCMT IO System -> TCMT IO System
forall a b. (a -> b) -> a -> b
$ QName -> [VerboseLevel] -> Type -> [Clause] -> TCMT IO System
checkSystemCoverage QName
name (IntSet -> [VerboseLevel]
IntSet.toList IntSet
isOneIxs) Type
fullType [Clause]
cs
                 Tele (Dom Type)
tel <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
                 let c :: Clause
c = Clause :: Range
-> Range
-> Tele (Dom Type)
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause
                       { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                       , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                       , clauseTel :: Tele (Dom Type)
clauseTel = Tele (Dom Type)
tel
                       , namedClausePats :: NAPs
namedClausePats = Tele (Dom Type) -> NAPs
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
tel
                       , clauseBody :: Maybe Term
clauseBody = Maybe Term
forall a. Maybe a
Nothing
                       , clauseType :: Maybe (Arg Type)
clauseType = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Type -> Arg Type
forall a. a -> Arg a
defaultArg Type
t)
                       , clauseCatchall :: Bool
clauseCatchall = Bool
False
                       , clauseRecursive :: Maybe Bool
clauseRecursive = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                       , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                       , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
                       }
                 ([Clause], Maybe System) -> TCMT IO ([Clause], Maybe System)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
cs [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause
c], System -> Maybe System
forall (f :: * -> *) a. Applicative f => a -> f a
pure System
sys)

        -- Annotate the clauses with which arguments are actually used.
        [Clause]
cs <- [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull {- =<< mapM rebindClause -} [Clause]
cs
        -- Andreas, 2010-11-12
        -- rebindClause is the identity, and instantiateFull eta-contracts
        -- removing this eta-contraction fixes issue 361
        -- however, Data.Star.Decoration.gmapAll no longer type-checks
        -- possibly due to missing eta-contraction!?

        -- Check if the function is injective.
        -- Andreas, 2015-07-01 we do it here in order to resolve metas
        -- in mutual definitions, e.g. the U/El definition in succeed/Issue439.agda
        -- We do it again for the mutual block after termination checking, see Rules.Decl.
        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.def" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"checkFunDef': checking injectivity..."
        FunctionInverse
inv <- Account Phase -> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Injectivity] (TCMT IO FunctionInverse -> TCMT IO FunctionInverse)
-> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
forall a b. (a -> b) -> a -> b
$
          QName -> [Clause] -> TCMT IO FunctionInverse
checkInjectivity QName
name [Clause]
cs

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"clauses before compilation"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QNamed Clause -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QNamed Clause -> TCM Doc)
-> (Clause -> QNamed Clause) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs
              ]

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.raw" VerboseLevel
65 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"clauses before compilation"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Clause -> VerboseKey) -> Clause -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [Clause]
cs
              ]

        -- add clauses for the coverage (& confluence) checker (needs to reduce)
        TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> TCM ()
addClauses QName
name [Clause]
cs

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.type" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  type   : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Type -> VerboseKey) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow) Type
t
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.type" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  context: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Tele (Dom Type) -> VerboseKey) -> Tele (Dom Type) -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Tele (Dom Type) -> TCM Doc)
-> TCMT IO (Tele (Dom Type)) -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)

        Type
fullType <- (Tele (Dom Type) -> Type -> Type)
-> Type -> Tele (Dom Type) -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Tele (Dom Type) -> Type -> Type
telePi Type
t (Tele (Dom Type) -> Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope

        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
"tc.cc.type" VerboseLevel
80 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show Type
fullType

        -- Coverage check and compile the clauses
        (Maybe SplitTree
mst, Bool
_recordExpressionBecameCopatternLHS, CompiledClauses
cc) <- Account Phase
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Coverage] (TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
 -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses))
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall a b. (a -> b) -> a -> b
$
          TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
 -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses))
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall a b. (a -> b) -> a -> b
$ Maybe (QName, Type)
-> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
compileClauses (if Bool
isSystem then Maybe (QName, Type)
forall a. Maybe a
Nothing else ((QName, Type) -> Maybe (QName, Type)
forall a. a -> Maybe a
Just (QName
name, Type
fullType)))
                                        [Clause]
cs
        -- Andreas, 2019-10-21 (see also issue #4142):
        -- We ignore whether the clause compilation turned some
        -- record expressions into copatterns
        -- (_recordExpressionsBecameCopatternLHS),
        -- since the defCopatternLHS flag is anyway set by traversing
        -- the compiled clauses looking for a copattern match
        -- (hasProjectionPatterns).

        -- Clause compilation runs the coverage checker, which might add
        -- some extra clauses.
        [Clause]
cs <- Definition -> [Clause]
defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"compiled clauses of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty CompiledClauses
cc
              ]

        -- The macro tag might be on the type signature
        Bool
ismacro <- Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name

        [Clause]
covering <- Defn -> [Clause]
funCovering (Defn -> [Clause])
-> (Definition -> Defn) -> Definition -> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name

        -- Jesper, 2019-05-30: if the constructors used in the
        -- lhs of a clause have rewrite rules, we need to check
        -- confluence here
        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optConfluenceCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [(Clause, VerboseLevel)]
-> ((Clause, VerboseLevel) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Clause] -> [VerboseLevel] -> [(Clause, VerboseLevel)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Clause]
cs [VerboseLevel
0..]) (((Clause, VerboseLevel) -> TCM ()) -> TCM ())
-> ((Clause, VerboseLevel) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \(Clause
c , VerboseLevel
clauseNo) ->
            QName -> VerboseLevel -> Clause -> TCM ()
checkConfluenceOfClause QName
name VerboseLevel
clauseNo Clause
c

        -- Add the definition
        TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
name (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          -- If there was a pragma for this definition, we can set the
          -- funTerminates field directly.
          Defn
defn <- Defn -> TCM Defn
autoInline (Defn -> TCM Defn) -> Defn -> TCM Defn
forall a b. (a -> b) -> a -> b
$
             Lens' Bool Defn -> LensSet Bool Defn
forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funMacro (Bool
ismacro Bool -> Bool -> Bool
|| DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$
             Defn
emptyFunction
             { funClauses :: [Clause]
funClauses        = [Clause]
cs
             , funCompiled :: Maybe CompiledClauses
funCompiled       = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc
             , funSplitTree :: Maybe SplitTree
funSplitTree      = Maybe SplitTree
mst
             , funDelayed :: Delayed
funDelayed        = Delayed
delayed
             , funInv :: FunctionInverse
funInv            = FunctionInverse
inv
             , funAbstr :: IsAbstract
funAbstr          = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
             , funExtLam :: Maybe ExtLamInfo
funExtLam         = (\ ExtLamInfo
e -> ExtLamInfo
e { extLamSys :: Maybe System
extLamSys = Maybe System
sys }) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extlam
             , funWith :: Maybe QName
funWith           = Maybe QName
with
             , funCovering :: [Clause]
funCovering       = [Clause]
covering
             }
          Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$
            (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
forall a b. a -> b -> a
const (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Bool
hasProjectionPatterns CompiledClauses
cc) (Definition -> Definition) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$
            ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
ai QName
name Type
fullType Defn
defn

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.def.fun" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"added " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> TCM Doc) -> (Definition -> Type) -> Definition -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCM Doc) -> TCMT IO Definition -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
              ]

-- | Set 'funTerminates' according to termination info in 'TCEnv',
--   which comes from a possible termination pragma.
useTerPragma :: Definition -> TCM Definition
useTerPragma :: Definition -> TCMT IO Definition
useTerPragma def :: Definition
def@Defn{ defName :: Definition -> QName
defName = QName
name, theDef :: Definition -> Defn
theDef = fun :: Defn
fun@Function{}} = do
  TerminationCheck ()
tc <- Lens' (TerminationCheck ()) TCEnv -> TCMT IO (TerminationCheck ())
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (TerminationCheck ()) TCEnv
eTerminationCheck
  let terminates :: Maybe Bool
terminates = case TerminationCheck ()
tc of
        TerminationCheck ()
NonTerminating -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        TerminationCheck ()
Terminating    -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        TerminationCheck ()
_              -> Maybe Bool
forall a. Maybe a
Nothing
  VerboseKey -> VerboseLevel -> [VerboseKey] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"tc.fundef" VerboseLevel
30 ([VerboseKey] -> TCM ()) -> [VerboseKey] -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [ VerboseKey
"funTerminates of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
name VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" set to " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe Bool -> VerboseKey
forall a. Show a => a -> VerboseKey
show Maybe Bool
terminates
    , VerboseKey
"  tc = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ TerminationCheck () -> VerboseKey
forall a. Show a => a -> VerboseKey
show TerminationCheck ()
tc
    ]
  Definition -> TCMT IO Definition
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ Definition
def { theDef :: Defn
theDef = Defn
fun { funTerminates :: Maybe Bool
funTerminates = Maybe Bool
terminates }}
useTerPragma Definition
def = Definition -> TCMT IO Definition
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def

-- | Insert some with-patterns into the with-clauses LHS of the given RHS.
-- (Used for @rewrite@.)
insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS
insertPatterns :: [Pattern' Expr] -> RHS -> RHS
insertPatterns [Pattern' Expr]
pats = \case
  A.WithRHS QName
aux [WithHiding Expr]
es [Clause]
cs -> QName -> [WithHiding Expr] -> [Clause] -> RHS
A.WithRHS QName
aux [WithHiding Expr]
es ([Clause] -> RHS) -> [Clause] -> RHS
forall a b. (a -> b) -> a -> b
$ [Clause] -> (Clause -> Clause) -> [Clause]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Clause]
cs ((Clause -> Clause) -> [Clause]) -> (Clause -> Clause) -> [Clause]
forall a b. (a -> b) -> a -> b
$
    \ (A.Clause (A.LHS LHSInfo
info LHSCore' Expr
core)                              [ProblemEq]
spats RHS
rhs                       WhereDeclarations
ds Bool
catchall) ->
       LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
info ([Pattern' Expr] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Pattern' Expr]
pats LHSCore' Expr
core)) [ProblemEq]
spats ([Pattern' Expr] -> RHS -> RHS
insertPatterns [Pattern' Expr]
pats RHS
rhs) WhereDeclarations
ds Bool
catchall
  A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats ([Pattern' Expr] -> RHS -> RHS
insertPatterns [Pattern' Expr]
pats RHS
rhs) WhereDeclarations
wh
  rhs :: RHS
rhs@RHS
A.AbsurdRHS -> RHS
rhs
  rhs :: RHS
rhs@A.RHS{}     -> RHS
rhs

-- | Insert with-patterns before the trailing with patterns.
-- If there are none, append the with-patterns.
insertPatternsLHSCore :: [A.Pattern] -> A.LHSCore -> A.LHSCore
insertPatternsLHSCore :: [Pattern' Expr] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Pattern' Expr]
pats = \case
  A.LHSWith LHSCore' Expr
core [Pattern' Expr]
wps [] -> LHSCore' Expr
-> [Pattern' Expr] -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e.
LHSCore' e -> [Pattern' e] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core ([Pattern' Expr]
pats [Pattern' Expr] -> [Pattern' Expr] -> [Pattern' Expr]
forall a. [a] -> [a] -> [a]
++ [Pattern' Expr]
wps) []
  LHSCore' Expr
core                  -> LHSCore' Expr
-> [Pattern' Expr] -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e.
LHSCore' e -> [Pattern' e] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core [Pattern' Expr]
pats []

-- | Parameters for creating a @with@-function.
data WithFunctionProblem
  = NoWithFunction
  | WithFunction
    { WithFunctionProblem -> QName
wfParentName :: QName                             -- ^ Parent function name.
    , WithFunctionProblem -> QName
wfName       :: QName                             -- ^ With function name.
    , WithFunctionProblem -> Type
wfParentType :: Type                              -- ^ Type of the parent function.
    , WithFunctionProblem -> Tele (Dom Type)
wfParentTel  :: Telescope                         -- ^ Context of the parent patterns.
    , WithFunctionProblem -> Tele (Dom Type)
wfBeforeTel  :: Telescope                         -- ^ Types of arguments to the with function before the with expressions (needed vars).
    , WithFunctionProblem -> Tele (Dom Type)
wfAfterTel   :: Telescope                         -- ^ Types of arguments to the with function after the with expressions (unneeded vars).
    , WithFunctionProblem -> [WithHiding (Term, EqualityView)]
wfExprs      :: [WithHiding (Term, EqualityView)] -- ^ With and rewrite expressions and their types.
    , WithFunctionProblem -> Type
wfRHSType    :: Type                              -- ^ Type of the right hand side.
    , WithFunctionProblem -> NAPs
wfParentPats :: [NamedArg DeBruijnPattern]        -- ^ Parent patterns.
    , WithFunctionProblem -> VerboseLevel
wfParentParams :: Nat                             -- ^ Number of module parameters in parent patterns
    , WithFunctionProblem -> Permutation
wfPermSplit  :: Permutation                       -- ^ Permutation resulting from splitting the telescope into needed and unneeded vars.
    , WithFunctionProblem -> Permutation
wfPermParent :: Permutation                       -- ^ Permutation reordering the variables in the parent pattern.
    , WithFunctionProblem -> Permutation
wfPermFinal  :: Permutation                       -- ^ Final permutation (including permutation for the parent clause).
    , WithFunctionProblem -> [Clause]
wfClauses    :: [A.Clause]                        -- ^ The given clauses for the with function
    }

checkSystemCoverage
  :: QName
  -> [Int]
  -> Type
  -> [Clause]
  -> TCM System
checkSystemCoverage :: QName -> [VerboseLevel] -> Type -> [Clause] -> TCMT IO System
checkSystemCoverage QName
f [VerboseLevel
n] Type
t [Clause]
cs = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sys.cover" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ((VerboseLevel, VerboseLevel) -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel
n , [Clause] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Clause]
cs)) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
  TelV Tele (Dom Type)
gamma Type
t <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpTo VerboseLevel
n Type
t
  Tele (Dom Type) -> TCMT IO System -> TCMT IO System
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma (TCMT IO System -> TCMT IO System)
-> TCMT IO System -> TCMT IO System
forall a b. (a -> b) -> a -> b
$ do
  TelV (ExtendTel Dom Type
a Abs (Tele (Dom Type))
_) Type
_ <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpTo VerboseLevel
1 Type
t
  Term
a <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a

  case Term
a of
    Def QName
q [Apply Arg Term
phi] -> do
      [Maybe QName
iz,Maybe QName
io] <- (VerboseKey -> TCMT IO (Maybe QName))
-> [VerboseKey] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VerboseKey -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinName' [VerboseKey
builtinIZero, VerboseKey
builtinIOne]
      Term
ineg <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
      Term
imin <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
      Term
imax <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
      Term
i0 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      Term
i1 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
      let
        isDir :: Pattern' x -> Maybe Bool
isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
iz = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
io = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        isDir Pattern' x
_ = Maybe Bool
forall a. Maybe a
Nothing

        collectDirs :: [Int] -> [DeBruijnPattern] -> [(Int,Bool)]
        collectDirs :: [VerboseLevel] -> [Pattern' DBPatVar] -> [(VerboseLevel, Bool)]
collectDirs [] [] = []
        collectDirs (VerboseLevel
i : [VerboseLevel]
is) (Pattern' DBPatVar
p : [Pattern' DBPatVar]
ps) | Just Bool
d <- Pattern' DBPatVar -> Maybe Bool
forall x. Pattern' x -> Maybe Bool
isDir Pattern' DBPatVar
p = (VerboseLevel
i,Bool
d) (VerboseLevel, Bool)
-> [(VerboseLevel, Bool)] -> [(VerboseLevel, Bool)]
forall a. a -> [a] -> [a]
: [VerboseLevel] -> [Pattern' DBPatVar] -> [(VerboseLevel, Bool)]
collectDirs [VerboseLevel]
is [Pattern' DBPatVar]
ps
                                      | Bool
otherwise         = [VerboseLevel] -> [Pattern' DBPatVar] -> [(VerboseLevel, Bool)]
collectDirs [VerboseLevel]
is [Pattern' DBPatVar]
ps
        collectDirs [VerboseLevel]
_ [Pattern' DBPatVar]
_ = [(VerboseLevel, Bool)]
forall a. HasCallStack => a
__IMPOSSIBLE__

        dir :: (Int,Bool) -> Term
        dir :: (VerboseLevel, Bool) -> Term
dir (VerboseLevel
i,Bool
False) = Term
ineg Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i]
        dir (VerboseLevel
i,Bool
True) = VerboseLevel -> Term
var VerboseLevel
i

        -- andI and orI have cases for singletons to improve error messages.
        andI, orI :: [Term] -> Term
        andI :: [Term] -> Term
andI [] = Term
i1
        andI [Term
t] = Term
t
        andI (Term
t:[Term]
ts) = (\ Term
x -> Term
imin Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
t, Term -> Arg Term
forall a. a -> Arg a
argN Term
x]) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
andI [Term]
ts

        orI :: [Term] -> Term
orI [] = Term
i0
        orI [Term
t] = Term
t
        orI (Term
t:[Term]
ts) = Term
imax Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
t, Term -> Arg Term
forall a. a -> Arg a
argN ([Term] -> Term
orI [Term]
ts)]

      let
        pats :: [[Pattern' DBPatVar]]
pats = (Clause -> [Pattern' DBPatVar])
-> [Clause] -> [[Pattern' DBPatVar]]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> [Pattern' DBPatVar] -> [Pattern' DBPatVar]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
n ([Pattern' DBPatVar] -> [Pattern' DBPatVar])
-> (Clause -> [Pattern' DBPatVar]) -> Clause -> [Pattern' DBPatVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (Pattern' DBPatVar) -> Pattern' DBPatVar)
-> NAPs -> [Pattern' DBPatVar]
forall a b. (a -> b) -> [a] -> [b]
map (Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar
forall name a. Named name a -> a
namedThing (Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar)
-> (NamedArg (Pattern' DBPatVar)
    -> Named NamedName (Pattern' DBPatVar))
-> NamedArg (Pattern' DBPatVar)
-> Pattern' DBPatVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' DBPatVar) -> Named NamedName (Pattern' DBPatVar)
forall e. Arg e -> e
unArg) (NAPs -> [Pattern' DBPatVar])
-> (Clause -> NAPs) -> Clause -> [Pattern' DBPatVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats) [Clause]
cs
        alphas :: [[(Int,Bool)]] -- the face maps corresponding to each clause
        alphas :: [[(VerboseLevel, Bool)]]
alphas = ([Pattern' DBPatVar] -> [(VerboseLevel, Bool)])
-> [[Pattern' DBPatVar]] -> [[(VerboseLevel, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map ([VerboseLevel] -> [Pattern' DBPatVar] -> [(VerboseLevel, Bool)]
collectDirs (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
n)) [[Pattern' DBPatVar]]
pats
        phis :: [Term] -- the φ terms for each clause (i.e. the alphas as terms)
        phis :: [Term]
phis = ([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map [Term] -> Term
andI ([[Term]] -> [Term]) -> [[Term]] -> [Term]
forall a b. (a -> b) -> a -> b
$ ([(VerboseLevel, Bool)] -> [Term])
-> [[(VerboseLevel, Bool)]] -> [[Term]]
forall a b. (a -> b) -> [a] -> [b]
map (((VerboseLevel, Bool) -> Term) -> [(VerboseLevel, Bool)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Bool) -> Term
dir) [[(VerboseLevel, Bool)]]
alphas
        psi :: Term
psi = [Term] -> Term
orI ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
phis
        pcs :: [(Term, Clause)]
pcs = [Term] -> [Clause] -> [(Term, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
phis [Clause]
cs
        boolToI :: Bool -> Term
boolToI Bool
True = Term
i1
        boolToI Bool
False = Term
i0

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sys.cover" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ([Pattern' DBPatVar] -> TCM Doc)
-> [[Pattern' DBPatVar]] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Pattern' DBPatVar] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [[Pattern' DBPatVar]]
pats
      Type
interval <- TCMT IO Term -> TCMT IO Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
elInf TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sys.cover" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"equalTerm " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
psi
      Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
interval (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi) Term
psi

      [[(Term, Clause)]] -> ([(Term, Clause)] -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([[(Term, Clause)]] -> [[(Term, Clause)]]
forall a. [a] -> [a]
init ([[(Term, Clause)]] -> [[(Term, Clause)]])
-> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a b. (a -> b) -> a -> b
$ [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a. [a] -> [a]
init ([[(Term, Clause)]] -> [[(Term, Clause)]])
-> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a b. (a -> b) -> a -> b
$ [(Term, Clause)] -> [[(Term, Clause)]]
forall a. [a] -> [[a]]
List.tails [(Term, Clause)]
pcs) (([(Term, Clause)] -> TCM ()) -> TCM ())
-> ([(Term, Clause)] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ ((Term
phi1,Clause
cl1):[(Term, Clause)]
pcs') -> do
        [(Term, Clause)] -> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Term, Clause)]
pcs' (((Term, Clause) -> TCMT IO [()]) -> TCM ())
-> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
phi2,Clause
cl2) -> do
          Term
phi12 <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
imin Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
phi1, Term -> Arg Term
forall a. a -> Arg a
argN Term
phi2])
          Term
-> (Map VerboseLevel Bool -> MetaId -> Term -> TCM ())
-> (Substitution -> TCM ())
-> TCMT IO [()]
forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (Map VerboseLevel Bool -> MetaId -> Term -> m a)
-> (Substitution -> m a)
-> m [a]
forallFaceMaps Term
phi12 (\ Map VerboseLevel Bool
_ MetaId
_ -> Term -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__) ((Substitution -> TCM ()) -> TCMT IO [()])
-> (Substitution -> TCM ()) -> TCMT IO [()]
forall a b. (a -> b) -> a -> b
$ \ Substitution
sigma -> do
            let args :: Args
args = Substitution
sigma Substitution -> Args -> Args
forall t a. Subst t a => Substitution' t -> a -> a
`applySubst` Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
                t' :: Type
t' = Substitution
sigma Substitution -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
`applySubst` Type
t
                fromReduced :: Reduced (Blocked p) p -> p
fromReduced (YesReduction Simplification
_ p
x) = p
x
                fromReduced (NoReduction Blocked p
x) = Blocked p -> p
forall t. Blocked t -> t
ignoreBlocking Blocked p
x
                body :: Clause -> TCMT IO Term
body Clause
cl = do
                  let extra :: VerboseLevel
extra = NAPs -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (VerboseLevel -> NAPs -> NAPs
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl)
                  TelV Tele (Dom Type)
delta Type
_ <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpTo VerboseLevel
extra Type
t'
                  (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
delta) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Term -> TCMT IO Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
                    (Reduced (Blocked Term) Term -> Term)
-> TCMT IO (Reduced (Blocked Term) Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reduced (Blocked Term) Term -> Term
forall p. Reduced (Blocked p) p -> p
fromReduced (TCMT IO (Reduced (Blocked Term) Term) -> TCMT IO Term)
-> TCMT IO (Reduced (Blocked Term) Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ReduceM (Reduced (Blocked Term) Term)
-> TCMT IO (Reduced (Blocked Term) Term)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Reduced (Blocked Term) Term)
 -> TCMT IO (Reduced (Blocked Term) Term))
-> ReduceM (Reduced (Blocked Term) Term)
-> TCMT IO (Reduced (Blocked Term) Term)
forall a b. (a -> b) -> a -> b
$
                      Term
-> [Clause]
-> RewriteRules
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked Term) Term)
appDef' (QName -> Elims -> Term
Def QName
f []) [Clause
cl] [] ((Arg Term -> MaybeReduced (Arg Term)) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced (Args -> MaybeReducedArgs) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Args -> Args
forall t a. Subst t a => VerboseLevel -> a -> a
raise (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) Args
args Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
delta)
            Term
v1 <- Clause -> TCMT IO Term
body Clause
cl1
            Term
v2 <- Clause -> TCMT IO Term
body Clause
cl2
            Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t' Term
v1 Term
v2

      [([(Term, Bool)], Term)]
sys <- [([(VerboseLevel, Bool)], Clause)]
-> (([(VerboseLevel, Bool)], Clause)
    -> TCMT IO ([(Term, Bool)], Term))
-> TCMT IO [([(Term, Bool)], Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([[(VerboseLevel, Bool)]]
-> [Clause] -> [([(VerboseLevel, Bool)], Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[(VerboseLevel, Bool)]]
alphas [Clause]
cs) ((([(VerboseLevel, Bool)], Clause)
  -> TCMT IO ([(Term, Bool)], Term))
 -> TCMT IO [([(Term, Bool)], Term)])
-> (([(VerboseLevel, Bool)], Clause)
    -> TCMT IO ([(Term, Bool)], Term))
-> TCMT IO [([(Term, Bool)], Term)]
forall a b. (a -> b) -> a -> b
$ \ ([(VerboseLevel, Bool)]
alpha,Clause
cl) -> do

            let
                -- Δ = Γ_α , Δ'α
                delta :: Tele (Dom Type)
delta = Clause -> Tele (Dom Type)
clauseTel Clause
cl
                -- Δ ⊢ b
                Just Term
b = Clause -> Maybe Term
clauseBody Clause
cl
                -- Δ ⊢ ps : Γ , o : [φ] , Δ'
                -- we assume that there's no pattern matching other
                -- than from the system
                ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
cl
                extra :: VerboseLevel
extra = NAPs -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (VerboseLevel -> NAPs -> NAPs
forall a. VerboseLevel -> [a] -> [a]
drop (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
gamma VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) NAPs
ps)
                -- size Δ'α = size Δ' = extra
                -- Γ , α ⊢ u
                takeLast :: VerboseLevel -> [a] -> [a]
takeLast VerboseLevel
n [a]
xs = VerboseLevel -> [a] -> [a]
forall a. VerboseLevel -> [a] -> [a]
drop ([a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
xs VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) [a]
xs
                weak :: [VerboseLevel] -> Substitution' a
weak [] = Substitution' a
forall a. Substitution' a
idS
                weak (VerboseLevel
i:[VerboseLevel]
is) = [VerboseLevel] -> Substitution' a
weak [VerboseLevel]
is Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` VerboseLevel -> Substitution' a -> Substitution' a
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS VerboseLevel
i (VerboseLevel -> Substitution' a
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
1)
                tel :: Tele (Dom Type)
tel = [Dom (VerboseKey, Type)] -> Tele (Dom Type)
telFromList (VerboseLevel
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. VerboseLevel -> [a] -> [a]
takeLast VerboseLevel
extra (Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
delta))
                u :: Term
u = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS VerboseLevel
extra ([VerboseLevel] -> Substitution
forall a. Subst a a => [VerboseLevel] -> Substitution' a
weak ([VerboseLevel] -> Substitution) -> [VerboseLevel] -> Substitution
forall a b. (a -> b) -> a -> b
$ [VerboseLevel] -> [VerboseLevel]
forall a. Ord a => [a] -> [a]
List.sort ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ ((VerboseLevel, Bool) -> VerboseLevel)
-> [(VerboseLevel, Bool)] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Bool) -> VerboseLevel
forall a b. (a, b) -> a
fst [(VerboseLevel, Bool)]
alpha) Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
`applySubst` Term
b)
            ([(Term, Bool)], Term) -> TCMT IO ([(Term, Bool)], Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (((VerboseLevel, Bool) -> (Term, Bool))
-> [(VerboseLevel, Bool)] -> [(Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseLevel -> Term) -> (VerboseLevel, Bool) -> (Term, Bool)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first VerboseLevel -> Term
var) [(VerboseLevel, Bool)]
alpha,Term
u)

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sys.cover.sys" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
gamma TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (([(Term, Bool)], Term) -> TCM Doc)
-> [([(Term, Bool)], Term)] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([(Term, Bool)], Term) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [([(Term, Bool)], Term)]
sys
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.sys.cover.sys" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Tele (Dom Type) -> VerboseKey) -> Tele (Dom Type) -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Tele (Dom Type)
gamma TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (([(Term, Bool)], Term) -> TCM Doc)
-> [([(Term, Bool)], Term)] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (([(Term, Bool)], Term) -> VerboseKey)
-> ([(Term, Bool)], Term)
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Term, Bool)], Term) -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [([(Term, Bool)], Term)]
sys
      System -> TCMT IO System
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type) -> [([(Term, Bool)], Term)] -> System
System Tele (Dom Type)
gamma [([(Term, Bool)], Term)]
sys) -- gamma uses names from the type, not the patterns, could we do better?
    Term
_ -> TCMT IO System
forall a. HasCallStack => a
__IMPOSSIBLE__
checkSystemCoverage QName
_ [VerboseLevel]
_ Type
t [Clause]
cs = TCMT IO System
forall a. HasCallStack => a
__IMPOSSIBLE__


-- * Info that is needed after all clauses have been processed.

data ClausesPostChecks = CPC
    { ClausesPostChecks -> IntSet
cpcPartialSplits :: IntSet
      -- ^ Which argument indexes have a partial split.
    }

instance Semigroup ClausesPostChecks where
  CPC IntSet
xs <> :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
<> CPC IntSet
xs' = IntSet -> ClausesPostChecks
CPC (IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs IntSet
xs')

instance Monoid ClausesPostChecks where
  mempty :: ClausesPostChecks
mempty  = IntSet -> ClausesPostChecks
CPC IntSet
forall a. Null a => a
empty
  mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
mappend = ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
forall a. Semigroup a => a -> a -> a
(<>)

-- | The LHS part of checkClause.
checkClauseLHS :: Type -> Maybe Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClauseLHS :: Type
-> Maybe Substitution
-> Clause' SpineLHS
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
withSub c :: Clause' SpineLHS
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
rhs0 WhereDeclarations
wh Bool
catchall) LHSResult -> TCM a
ret = do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.top" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking clause" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Clause' SpineLHS -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Clause' SpineLHS
c
    [NamedArg (Pattern' Expr)]
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
trailingWithPatterns [NamedArg (Pattern' Expr)]
aps) (([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ())
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [NamedArg (Pattern' Expr)]
withPats -> do
      TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Pattern' Expr] -> TypeError
UnexpectedWithPatterns ([Pattern' Expr] -> TypeError) -> [Pattern' Expr] -> TypeError
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> Pattern' Expr)
-> [NamedArg (Pattern' Expr)] -> [Pattern' Expr]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg [NamedArg (Pattern' Expr)]
withPats
    Call -> TCM a -> TCM a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Type -> Clause' SpineLHS -> Call
CheckClause Type
t Clause' SpineLHS
c) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
      [NamedArg (Pattern' Expr)]
aps <- [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg (Pattern' Expr)]
aps
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [ProblemEq] -> Bool
forall a. Null a => a -> Bool
null [ProblemEq]
strippedPats) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.top" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"strippedPats:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ Pattern' Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern' Expr
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a | A.ProblemEq Pattern' Expr
p Term
v Dom Type
a <- [ProblemEq]
strippedPats ]
      Type
closed_t <- (Tele (Dom Type) -> Type -> Type)
-> Type -> Tele (Dom Type) -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Type
t (Tele (Dom Type) -> Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      Call
-> Maybe QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
forall a.
Call
-> Maybe QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide (SpineLHS -> Call
CheckLHS SpineLHS
lhs) (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x) [NamedArg (Pattern' Expr)]
aps Type
t Maybe Substitution
withSub [ProblemEq]
strippedPats LHSResult -> TCM a
ret

-- | Type check a function clause.

checkClause
  :: Type          -- ^ Type of function defined by this clause.
  -> Maybe Substitution  -- ^ Module parameter substitution arising from with-abstraction.
  -> A.SpineClause -- ^ Clause.
  -> TCM (Clause,ClausesPostChecks)  -- ^ Type-checked clause

checkClause :: Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe Substitution
withSub c :: Clause' SpineLHS
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
rhs0 WhereDeclarations
wh Bool
catchall) = do
  [Name]
cxtNames <- [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name])
-> ([Dom' Term (Name, Type)] -> [Name])
-> [Dom' Term (Name, Type)]
-> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term (Name, Type) -> Name)
-> [Dom' Term (Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Name])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
  Type
-> Maybe Substitution
-> Clause' SpineLHS
-> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
Type
-> Maybe Substitution
-> Clause' SpineLHS
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
withSub Clause' SpineLHS
c ((LHSResult -> TCMT IO (Clause, ClausesPostChecks))
 -> TCMT IO (Clause, ClausesPostChecks))
-> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ \ lhsResult :: LHSResult
lhsResult@(LHSResult VerboseLevel
npars Tele (Dom Type)
delta NAPs
ps Bool
absurdPat Arg Type
trhs Substitution
patSubst [AsBinding]
asb IntSet
psplit) -> do
        -- Note that we might now be in irrelevant context,
        -- in case checkLeftHandSide walked over an irrelevant projection pattern.

        -- Subtle: checkRHS expects the function type to be the lambda lifted
        -- type. If we're checking a with-function that's already the case,
        -- otherwise we need to abstract over the module telescope.
        Type
t' <- case Maybe Substitution
withSub of
                Just{}  -> Type -> TCMT IO Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
                Maybe Substitution
Nothing -> do
                  Tele (Dom Type)
theta <- ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (QName -> ModuleName
qnameModule QName
x)
                  Type -> TCMT IO Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
theta Type
t

        -- At this point we should update the named dots potential with-clauses
        -- in the right-hand side. When checking a clause we expect the named
        -- dots to live in the context of the closest parent lhs, but the named
        -- dots added by buildWithFunction live in the context of the
        -- with-function arguments before pattern matching. That's what we need
        -- patSubst for.
        let rhs :: RHS
rhs = RHS -> RHS
updateRHS RHS
rhs0
            updateRHS :: RHS -> RHS
updateRHS rhs :: RHS
rhs@A.RHS{}               = RHS
rhs
            updateRHS rhs :: RHS
rhs@A.AbsurdRHS{}         = RHS
rhs
            updateRHS (A.WithRHS QName
q [WithHiding Expr]
es [Clause]
cs)       = QName -> [WithHiding Expr] -> [Clause] -> RHS
A.WithRHS QName
q [WithHiding Expr]
es ((Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Clause
updateClause [Clause]
cs)
            updateRHS (A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) =
              [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes (Substitution -> [ProblemEq] -> [ProblemEq]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh

            updateClause :: Clause -> Clause
updateClause (A.Clause LHS
f [ProblemEq]
spats RHS
rhs WhereDeclarations
wh Bool
ca) =
              LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
f (Substitution -> [ProblemEq] -> [ProblemEq]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh Bool
ca

        (Maybe Term
body, WithFunctionProblem
with) <- [AsBinding]
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. WhereDeclarations -> TCM a -> TCM a
checkWhere WhereDeclarations
wh (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ LHSInfo
-> QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> LHSResult
-> RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps Type
t' LHSResult
lhsResult RHS
rhs

        -- Note that the with function doesn't necessarily share any part of
        -- the context with the parent (but withSub will take you from parent
        -- to child).

        TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.With] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction [Name]
cxtNames WithFunctionProblem
with

        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optDoubleCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Maybe Term
body of
          Just Term
v  -> do
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.top" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
              [ TCM Doc
"double checking rhs"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs))
              ]
            TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Comparison -> Type -> TCM ()
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> Type -> m ()
checkInternal Term
v Comparison
CmpLeq (Type -> TCM ()) -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs
          Maybe Term
Nothing -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.top" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"Clause before translation:"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ TCM Doc
"delta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta
            , TCM Doc
"ps    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [Doc] -> Doc
P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs -> TCMT IO [Doc]
forall (m :: * -> *). MonadPretty m => NAPs -> m [Doc]
prettyTCMPatterns NAPs
ps
            , TCM Doc
"body  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> (Term -> TCM Doc) -> Maybe Term -> TCM Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM Doc
"_|_" Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe Term
body
            , TCM Doc
"type  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            ]
          ]

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.top" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"Clause before translation (raw):"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ TCM Doc
"ps    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (NAPs -> VerboseKey
forall a. Show a => a -> VerboseKey
show NAPs
ps)
            , TCM Doc
"body  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Maybe Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Maybe Term
body)
            , TCM Doc
"type  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show Type
t)
            ]
          ]

        -- check naturality wrt the interval.
        let
          iApplyVars :: [NamedArg DeBruijnPattern] -> [(Int, (Term,Term))]
          iApplyVars :: NAPs -> [(VerboseLevel, (Term, Term))]
iApplyVars NAPs
ps = ((Pattern' DBPatVar -> [(VerboseLevel, (Term, Term))])
 -> [Pattern' DBPatVar] -> [(VerboseLevel, (Term, Term))])
-> [Pattern' DBPatVar]
-> (Pattern' DBPatVar -> [(VerboseLevel, (Term, Term))])
-> [(VerboseLevel, (Term, Term))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Pattern' DBPatVar -> [(VerboseLevel, (Term, Term))])
-> [Pattern' DBPatVar] -> [(VerboseLevel, (Term, Term))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((NamedArg (Pattern' DBPatVar) -> Pattern' DBPatVar)
-> NAPs -> [Pattern' DBPatVar]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' DBPatVar) -> Pattern' DBPatVar
forall a. NamedArg a -> a
namedArg NAPs
ps) ((Pattern' DBPatVar -> [(VerboseLevel, (Term, Term))])
 -> [(VerboseLevel, (Term, Term))])
-> (Pattern' DBPatVar -> [(VerboseLevel, (Term, Term))])
-> [(VerboseLevel, (Term, Term))]
forall a b. (a -> b) -> a -> b
$ \case
                             IApplyP PatternInfo
_ Term
t Term
u DBPatVar
x -> [(DBPatVar -> VerboseLevel
dbPatVarIndex DBPatVar
x,(Term
t,Term
u))]
                             VarP{} -> []
                             ProjP{}-> []
                             LitP{} -> []
                             DotP{} -> []
                             DefP PatternInfo
_ QName
_ NAPs
ps -> NAPs -> [(VerboseLevel, (Term, Term))]
iApplyVars NAPs
ps
                             ConP ConHead
_ ConPatternInfo
_ NAPs
ps -> NAPs -> [(VerboseLevel, (Term, Term))]
iApplyVars NAPs
ps

        -- compute body modification for irrelevant definitions, see issue 610
        Relevance
rel <- (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
        let bodyMod :: f Term -> f Term
bodyMod f Term
body = case Relevance
rel of
              Relevance
Irrelevant -> Term -> Term
dontCare (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Term
body
              Relevance
_          -> f Term
body

        -- absurd clauses don't define computational behaviour, so it's fine to
        -- treat them as catchalls.
        let catchall' :: Bool
catchall' = Bool
catchall Bool -> Bool -> Bool
|| Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
body

        (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ (, IntSet -> ClausesPostChecks
CPC IntSet
psplit)
          Clause :: Range
-> Range
-> Tele (Dom Type)
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause { clauseLHSRange :: Range
clauseLHSRange  = LHSInfo -> Range
forall t. HasRange t => t -> Range
getRange LHSInfo
i
                 , clauseFullRange :: Range
clauseFullRange = Clause' SpineLHS -> Range
forall t. HasRange t => t -> Range
getRange Clause' SpineLHS
c
                 , clauseTel :: Tele (Dom Type)
clauseTel       = KillRangeT (Tele (Dom Type))
forall a. KillRange a => KillRangeT a
killRange Tele (Dom Type)
delta
                 , namedClausePats :: NAPs
namedClausePats = NAPs
ps
                 , clauseBody :: Maybe Term
clauseBody      = Maybe Term -> Maybe Term
forall (f :: * -> *). Functor f => f Term -> f Term
bodyMod Maybe Term
body
                 , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just Arg Type
trhs
                 , clauseCatchall :: Bool
clauseCatchall  = Bool
catchall'
                 , clauseRecursive :: Maybe Bool
clauseRecursive   = Maybe Bool
forall a. Maybe a
Nothing -- we don't know yet
                 , clauseUnreachable :: Maybe Bool
clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing -- we don't know yet
                 , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis  = LHSInfo -> ExpandedEllipsis
lhsEllipsis LHSInfo
i
                 }

-- | Type check the @with@ and @rewrite@ lhss and/or the rhs.

checkRHS
  :: LHSInfo                 -- ^ Range of lhs.
  -> QName                   -- ^ Name of function.
  -> [NamedArg A.Pattern]    -- ^ Patterns in lhs.
  -> Type                    -- ^ Top-level type of function.
  -> LHSResult               -- ^ Result of type-checking patterns
  -> A.RHS                   -- ^ Rhs to check.
  -> TCM (Maybe Term, WithFunctionProblem)
                                              -- Note: the as-bindings are already bound (in checkClause)
checkRHS :: LHSInfo
-> QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> LHSResult
-> RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps Type
t lhsResult :: LHSResult
lhsResult@(LHSResult VerboseLevel
_ Tele (Dom Type)
delta NAPs
ps Bool
absurdPat Arg Type
trhs Substitution
_ [AsBinding]
_asb IntSet
_) RHS
rhs0 =
  RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs0 where

  handleRHS :: A.RHS -> TCM (Maybe Term, WithFunctionProblem)
  handleRHS :: RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs = case RHS
rhs of
    A.RHS Expr
e Maybe Expr
_                  -> Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS Expr
e
    RHS
A.AbsurdRHS                -> TCM (Maybe Term, WithFunctionProblem)
noRHS
    A.RewriteRHS [RewriteEqn]
eqs [ProblemEq]
ps RHS
rhs WhereDeclarations
wh -> [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [RewriteEqn]
eqs [ProblemEq]
ps RHS
rhs WhereDeclarations
wh
    A.WithRHS QName
aux [WithHiding Expr]
es [Clause]
cs        -> QName
-> [WithHiding Expr]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithHiding Expr]
es [Clause]
cs

  -- Ordinary case: f xs = e
  ordinaryRHS :: A.Expr -> TCM (Maybe Term, WithFunctionProblem)
  ordinaryRHS :: Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS Expr
e = Account Phase
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.CheckRHS] (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
    -- If there is an absurd pattern, we do not need a RHS. If we have
    -- one we complain, ignore it and return the same @(Nothing, NoWithFunction)@
    -- as the case dealing with @A.AbsurdRHS@.
    Maybe Term
mv <- if Bool
absurdPat
          then Maybe Term
forall a. Maybe a
Nothing Maybe Term -> TCM () -> TCMT IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Expr -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Expr
e (Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ NAPs -> Warning
AbsurdPatternRequiresNoRHS NAPs
ps)
          else Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> TCMT IO Term -> TCMT IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Type -> TCMT IO Term
checkExpr Expr
e (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs)
    (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
mv, WithFunctionProblem
NoWithFunction)

  -- Absurd case: no right hand side
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS = do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
absurdPat (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> TypeError
NoRHSRequiresAbsurdPattern [NamedArg (Pattern' Expr)]
aps
    (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing, WithFunctionProblem
NoWithFunction)


  -- With case: @f xs with a | b | c | ...; ... | ps1 = rhs1; ... | ps2 = rhs2; ...@
  -- This is mostly a wrapper around @checkWithRHS@
  withRHS :: QName               -- ^ name of the with-function
          -> [WithHiding A.Expr] -- ^ @[a, b, c, ...]@
          -> [A.Clause]          -- ^ @[(ps1 = rhs1), (ps2 = rhs), ...]@
          -> TCM (Maybe Term, WithFunctionProblem)
  withRHS :: QName
-> [WithHiding Expr]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithHiding Expr]
es [Clause]
cs = do

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ TCM Doc
"TC.Rules.Def.checkclause reached A.WithRHS"
      , [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA QName
aux TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (WithHiding Expr -> TCM Doc) -> [WithHiding Expr] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCM Doc -> TCM Doc)
-> (WithHiding Expr -> TCM Doc) -> WithHiding Expr -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithHiding Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA) [WithHiding Expr]
es
      ]
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseLevel
nfv <- TCM VerboseLevel
getCurrentModuleFreeVars
      ModuleName
m   <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
      [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"with function module:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
             [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Name -> TCM Doc) -> [Name] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Name] -> [TCM Doc]) -> [Name] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m)
          ,  VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"free variables: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
nfv
          ]

    -- Infer the types of the with expressions
    [WithHiding (Term, EqualityView)]
vtys <- (WithHiding Expr -> TCMT IO (WithHiding (Term, EqualityView)))
-> [WithHiding Expr] -> TCMT IO [WithHiding (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Expr -> TCMT IO (Term, EqualityView))
-> WithHiding Expr -> TCMT IO (WithHiding (Term, EqualityView))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType ((Term, Type) -> (Term, EqualityView))
-> (Expr -> TCMT IO (Term, Type))
-> Expr
-> TCMT IO (Term, EqualityView)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Expr -> TCMT IO (Term, Type)
inferExprForWith)) [WithHiding Expr]
es

    -- Andreas, 2016-01-23, Issue #1796
    -- Run the size constraint solver to improve with-abstraction
    -- in case the with-expression contains size metas.
    DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DefaultToInfty

    QName
-> QName
-> Type
-> LHSResult
-> [WithHiding (Term, EqualityView)]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type
t LHSResult
lhsResult [WithHiding (Term, EqualityView)]
vtys [Clause]
cs

  -- Rewrite case: f xs (rewrite / invert) a | b | c | ...
  rewriteEqnsRHS :: [A.RewriteEqn] -> [A.ProblemEq] -> A.RHS -> A.WhereDeclarations -> TCM (Maybe Term, WithFunctionProblem)
  rewriteEqnsRHS :: [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [] [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh = WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. WhereDeclarations -> TCM a -> TCM a
checkWhere WhereDeclarations
wh (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs
      -- Case: @rewrite@
      -- Andreas, 2014-01-17, Issue 1402:
      -- If the rewrites are discarded since lhs=rhs, then
      -- we can actually have where clauses.
  rewriteEqnsRHS (RewriteEqn
r:[RewriteEqn]
rs) [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh = case RewriteEqn
r of
    Rewrite ((QName
qname, Expr
eq) : [(QName, Expr)]
qes) ->
      QName
-> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS QName
qname Expr
eq (case [(QName, Expr)]
qes of { [] -> [RewriteEqn]
rs; [(QName, Expr)]
_ -> [(QName, Expr)] -> RewriteEqn
forall qn p e. [(qn, e)] -> RewriteEqn' qn p e
Rewrite [(QName, Expr)]
qes RewriteEqn -> [RewriteEqn] -> [RewriteEqn]
forall a. a -> [a] -> [a]
: [RewriteEqn]
rs })
    Invert QName
_     []  -> TCM (Maybe Term, WithFunctionProblem)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Invert QName
qname [(Pattern' Expr, Expr)]
pes -> QName
-> [(Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname [(Pattern' Expr, Expr)]
pes [RewriteEqn]
rs
    -- Invariant: these lists are non-empty
    Rewrite [] -> TCM (Maybe Term, WithFunctionProblem)
forall a. HasCallStack => a
__IMPOSSIBLE__

    where

    -- @invert@ clauses
    invertEqnRHS :: QName -> [(A.Pattern,A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    invertEqnRHS :: QName
-> [(Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname [(Pattern' Expr, Expr)]
pes [RewriteEqn]
rs = do

      let ([Pattern' Expr]
pats, [Expr]
es) = [(Pattern' Expr, Expr)] -> ([Pattern' Expr], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Pattern' Expr, Expr)]
pes
      -- Infer the types of the with expressions
      [WithHiding (Term, EqualityView)]
vtys <- (Expr -> TCMT IO (WithHiding (Term, EqualityView)))
-> [Expr] -> TCMT IO [WithHiding (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Hiding -> (Term, EqualityView) -> WithHiding (Term, EqualityView)
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
NotHidden ((Term, EqualityView) -> WithHiding (Term, EqualityView))
-> (Expr -> TCMT IO (Term, EqualityView))
-> Expr
-> TCMT IO (WithHiding (Term, EqualityView))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> (Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType ((Term, Type) -> (Term, EqualityView))
-> (Expr -> TCMT IO (Term, Type))
-> Expr
-> TCMT IO (Term, EqualityView)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Expr -> TCMT IO (Term, Type)
inferExprForWith) [Expr]
es

      -- Andreas, 2016-04-14, see also Issue #1796
      -- Run the size constraint solver to improve with-abstraction
      -- in case the with-expression contains size metas.
      DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DefaultToInfty

      let rhs' :: RHS
rhs' = [Pattern' Expr] -> RHS -> RHS
insertPatterns [Pattern' Expr]
pats RHS
rhs
          (RHS
rhs'', WhereDeclarations
outerWhere) -- the where clauses should go on the inner-most with
            | [RewriteEqn] -> Bool
forall a. Null a => a -> Bool
null [RewriteEqn]
rs  = (RHS
rhs', WhereDeclarations
wh)
            | Bool
otherwise = ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
rs [ProblemEq]
strippedPats RHS
rhs' WhereDeclarations
wh, WhereDeclarations
A.noWhereDecls)
          -- Andreas, 2014-03-05 kill range of copied patterns
          -- since they really do not have a source location.
          cl :: Clause
cl = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
forall a b. (a -> b) -> a -> b
$ [Pattern' Expr] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Pattern' Expr]
pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
-> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
forall a. KillRange a => KillRangeT a
killRange [NamedArg (Pattern' Expr)]
aps)
                 [ProblemEq]
strippedPats RHS
rhs'' WhereDeclarations
outerWhere Bool
False

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.invert" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text VerboseKey
"invert"
        , TCM Doc
"  rhs' = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (RHS -> VerboseKey) -> RHS -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RHS -> VerboseKey
forall a. Show a => a -> VerboseKey
show) RHS
rhs'
        ]
      QName
-> QName
-> Type
-> LHSResult
-> [WithHiding (Term, EqualityView)]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
qname Type
t LHSResult
lhsResult [WithHiding (Term, EqualityView)]
vtys [Clause
cl]

    -- @rewrite@ clauses
    rewriteEqnRHS :: QName -> A.Expr
                  -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnRHS :: QName
-> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS QName
qname Expr
eq [RewriteEqn]
rs = do

      -- Action for skipping this rewrite.
      -- We do not want to create unsolved metas in case of
      -- a futile rewrite with a reflexive equation.
      -- Thus, we restore the state in this case,
      -- unless the rewrite expression contains questionmarks.
      TCState
st <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      let recurse :: TCM (Maybe Term, WithFunctionProblem)
recurse = do
           TCState
st' <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
           -- Comparing the whole stInteractionPoints maps is a bit
           -- wasteful, but we assume
           -- 1. rewriting with a reflexive equality to happen rarely,
           -- 2. especially with ?-holes in the rewrite expression
           -- 3. and a large overall number of ?s.
           let sameIP :: TCState -> TCState -> Bool
sameIP = InteractionPoints -> InteractionPoints -> Bool
forall a. Eq a => a -> a -> Bool
(==) (InteractionPoints -> InteractionPoints -> Bool)
-> (TCState -> InteractionPoints) -> TCState -> TCState -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (TCState -> Lens' InteractionPoints TCState -> InteractionPoints
forall o i. o -> Lens' i o -> i
^.Lens' InteractionPoints TCState
stInteractionPoints)
           Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TCState -> TCState -> Bool
sameIP TCState
st TCState
st') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st
           RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS (RHS -> TCM (Maybe Term, WithFunctionProblem))
-> RHS -> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
rs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh

      -- Get value and type of rewrite-expression.

      (Term
proof, Type
eqt) <- Expr -> TCMT IO (Term, Type)
inferExpr Expr
eq

      -- Andreas, 2016-04-14, see also Issue #1796
      -- Run the size constraint solver to improve with-abstraction
      -- in case the with-expression contains size metas.
      DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DefaultToInfty

      -- Check that the type is actually an equality (lhs ≡ rhs)
      -- and extract lhs, rhs, and their type.

      Type
t' <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
eqt
      (EqualityView
eqt,Type
rewriteType,Term
rewriteFrom,Term
rewriteTo) <- Type -> TCM EqualityView
equalityView Type
t' TCM EqualityView
-> (EqualityView -> TCMT IO (EqualityView, Type, Term, Term))
-> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        eqt :: EqualityView
eqt@(EqualityType Sort
_s QName
_eq Args
_params (Arg ArgInfo
_ Term
dom) Arg Term
a Arg Term
b) -> do
          Sort
s <- Term -> TCMT IO Sort
forall (m :: * -> *). MonadCheckInternal m => Term -> m Sort
inferSort Term
dom
          (EqualityView, Type, Term, Term)
-> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView
eqt, Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s Term
dom, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b)
          -- Note: the sort _s of the equality need not be the sort of the type @dom@!
        OtherType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
-> (Doc -> TypeError)
-> Doc
-> TCMT IO (EqualityView, Type, Term, Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO (EqualityView, Type, Term, Term))
-> TCM Doc -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          TCM Doc
"Cannot rewrite by equation of type" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'

      -- Get the name of builtin REFL.

      Con ConHead
reflCon ConInfo
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
      Maybe ArgInfo
reflInfo <- (ArgInfo -> ArgInfo) -> Maybe ArgInfo -> Maybe ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) (Maybe ArgInfo -> Maybe ArgInfo)
-> TCMT IO (Maybe ArgInfo) -> TCMT IO (Maybe ArgInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
reflCon

      -- Andreas, 2017-01-11:
      -- The test for refl is obsolete after fixes of #520 and #1740.
      -- -- Andreas, 2014-05-17  Issue 1110:
      -- -- Rewriting with @refl@ has no effect, but gives an
      -- -- incomprehensible error message about the generated
      -- -- with clause. Thus, we rather do simply nothing if
      -- -- rewriting with @refl@ is attempted.
      -- let isReflProof = do
      --      v <- reduce proof
      --      case v of
      --        Con c _ [] | c == reflCon -> return True
      --        _ -> return False
      -- ifM isReflProof recurse $ {- else -} do

      -- Process 'rewrite' clause like a suitable 'with' clause.

      -- The REFL constructor might have an argument
      let reflPat :: Pattern' e
reflPat  = ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
reflCon) (NAPs e -> Pattern' e) -> NAPs e -> Pattern' e
forall a b. (a -> b) -> a -> b
$
            Maybe (Arg (Named NamedName (Pattern' e))) -> NAPs e
forall a. Maybe a -> [a]
maybeToList (Maybe (Arg (Named NamedName (Pattern' e))) -> NAPs e)
-> Maybe (Arg (Named NamedName (Pattern' e))) -> NAPs e
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Arg (Named NamedName (Pattern' e)))
-> Maybe ArgInfo -> Maybe (Arg (Named NamedName (Pattern' e)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ ArgInfo
ai -> ArgInfo
-> Named NamedName (Pattern' e)
-> Arg (Named NamedName (Pattern' e))
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named NamedName (Pattern' e)
 -> Arg (Named NamedName (Pattern' e)))
-> Named NamedName (Pattern' e)
-> Arg (Named NamedName (Pattern' e))
forall a b. (a -> b) -> a -> b
$ Pattern' e -> Named NamedName (Pattern' e)
forall a name. a -> Named name a
unnamed (Pattern' e -> Named NamedName (Pattern' e))
-> Pattern' e -> Named NamedName (Pattern' e)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) Maybe ArgInfo
reflInfo

      -- Andreas, 2015-12-25  Issue #1740:
      -- After the fix of #520, rewriting with a reflexive equation
      -- has to be desugared as matching against refl.
      let isReflexive :: TCMT IO Bool
isReflexive = TCM () -> TCMT IO Bool
forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
           Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
rewriteType Term
rewriteFrom Term
rewriteTo

      ([Pattern' Expr]
pats, Term
withExpr, EqualityView
withType) <- do
        TCMT IO Bool
-> TCMT IO ([Pattern' Expr], Term, EqualityView)
-> TCMT IO ([Pattern' Expr], Term, EqualityView)
-> TCMT IO ([Pattern' Expr], Term, EqualityView)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
isReflexive
          {-then-} (([Pattern' Expr], Term, EqualityView)
-> TCMT IO ([Pattern' Expr], Term, EqualityView)
forall (m :: * -> *) a. Monad m => a -> m a
return ([ Pattern' Expr
forall e. Pattern' e
reflPat ]                    , Term
proof, Type -> EqualityView
OtherType Type
t'))
          {-else-} (([Pattern' Expr], Term, EqualityView)
-> TCMT IO ([Pattern' Expr], Term, EqualityView)
forall (m :: * -> *) a. Monad m => a -> m a
return ([ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange, Pattern' Expr
forall e. Pattern' e
reflPat ], Term
proof, EqualityView
eqt))

      let rhs' :: RHS
rhs' = [Pattern' Expr] -> RHS -> RHS
insertPatterns [Pattern' Expr]
pats RHS
rhs
          (RHS
rhs'', WhereDeclarations
outerWhere) -- the where clauses should go on the inner-most with
            | [RewriteEqn] -> Bool
forall a. Null a => a -> Bool
null [RewriteEqn]
rs  = (RHS
rhs', WhereDeclarations
wh)
            | Bool
otherwise = ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
rs [ProblemEq]
strippedPats RHS
rhs' WhereDeclarations
wh, WhereDeclarations
A.noWhereDecls)
          -- Andreas, 2014-03-05 kill range of copied patterns
          -- since they really do not have a source location.
          cl :: Clause
cl = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
forall a b. (a -> b) -> a -> b
$ [Pattern' Expr] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Pattern' Expr]
pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
-> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
forall a. KillRange a => KillRangeT a
killRange [NamedArg (Pattern' Expr)]
aps)
                 [ProblemEq]
strippedPats RHS
rhs'' WhereDeclarations
outerWhere Bool
False

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rewrite" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text VerboseKey
"rewrite"
        , TCM Doc
"  rhs' = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (RHS -> VerboseKey) -> RHS -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RHS -> VerboseKey
forall a. Show a => a -> VerboseKey
show) RHS
rhs'
        ]
      QName
-> QName
-> Type
-> LHSResult
-> [WithHiding (Term, EqualityView)]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
qname Type
t LHSResult
lhsResult [Hiding -> (Term, EqualityView) -> WithHiding (Term, EqualityView)
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
NotHidden (Term
withExpr, EqualityView
withType)] [Clause
cl]

checkWithRHS
  :: QName                             -- ^ Name of function.
  -> QName                             -- ^ Name of the with-function.
  -> Type                              -- ^ Type of function.
  -> LHSResult                         -- ^ Result of type-checking patterns
  -> [WithHiding (Term, EqualityView)] -- ^ Expressions and types of with-expressions.
  -> [A.Clause]                        -- ^ With-clauses to check.
  -> TCM (Maybe Term, WithFunctionProblem)
                                -- Note: as-bindings already bound (in checkClause)
checkWithRHS :: QName
-> QName
-> Type
-> LHSResult
-> [WithHiding (Term, EqualityView)]
-> [Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type
t (LHSResult VerboseLevel
npars Tele (Dom Type)
delta NAPs
ps Bool
_absurdPat Arg Type
trhs Substitution
_ [AsBinding]
_asb IntSet
_) [WithHiding (Term, EqualityView)]
vtys0 [Clause]
cs =
  Account Phase
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.With] (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
        let withArgs :: [WithHiding Term]
withArgs = [WithHiding (Term, EqualityView)] -> [WithHiding Term]
withArguments [WithHiding (Term, EqualityView)]
vtys0
            perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ NAPs -> Maybe Permutation
dbPatPerm NAPs
ps
        [WithHiding (Term, EqualityView)]
vtys0 <- [WithHiding (Term, EqualityView)]
-> TCMT IO [WithHiding (Term, EqualityView)]
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise [WithHiding (Term, EqualityView)]
vtys0

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"delta  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta
          ]
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          -- declared locally because we do not want to use the unzip'd thing!
          let ([Term]
vs, [EqualityView]
as) = (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> [WithHiding (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing [WithHiding (Term, EqualityView)]
vtys0 in
          [ TCM Doc
"vs     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs
          , TCM Doc
"as     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [EqualityView] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [EqualityView]
as
          , TCM Doc
"perm   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm)
          ]

        -- Split the telescope into the part needed to type the with arguments
        -- and all the other stuff
        let (Tele (Dom Type)
delta1, Tele (Dom Type)
delta2, Permutation
perm', Type
t', [WithHiding (Term, EqualityView)]
vtys) = Tele (Dom Type)
-> Type
-> [WithHiding (Term, EqualityView)]
-> (Tele (Dom Type), Tele (Dom Type), Permutation, Type,
    [WithHiding (Term, EqualityView)])
splitTelForWith Tele (Dom Type)
delta (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs) [WithHiding (Term, EqualityView)]
vtys0
        let finalPerm :: Permutation
finalPerm = Permutation -> Permutation -> Permutation
composeP Permutation
perm' Permutation
perm

        VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.with.top" VerboseLevel
75 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"delta  = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom Type)
delta

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"delta1 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta1
          , TCM Doc
"delta2 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta2)
          ]
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"perm'  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm')
          , TCM Doc
"fPerm  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
finalPerm)
          ]

        -- Create the body of the original function

        -- All the context variables
        Args
us <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
        let n :: VerboseLevel
n = Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
us
            m :: VerboseLevel
m = Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta
            -- First the variables bound outside this definition
            (Args
us0, Args
us1') = VerboseLevel -> Args -> (Args, Args)
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
m) Args
us
            -- Then permute the rest and grab those needed to for the with arguments
            (Args
us1, Args
us2)  = VerboseLevel -> Args -> (Args, Args)
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta1) (Args -> (Args, Args)) -> Args -> (Args, Args)
forall a b. (a -> b) -> a -> b
$ Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute Permutation
perm' Args
us1'
            -- Now stuff the with arguments in between and finish with the remaining variables
            mkWithArg :: WithHiding a -> Arg a
mkWithArg = \ (WithHiding Hiding
h a
e) -> Hiding -> Arg a -> Arg a
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (Arg a -> Arg a) -> Arg a -> Arg a
forall a b. (a -> b) -> a -> b
$ a -> Arg a
forall a. a -> Arg a
defaultArg a
e
            v :: Term
v         = QName -> Elims -> Term
Def QName
aux (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Args
us0 Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
us1 Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ (WithHiding Term -> Arg Term) -> [WithHiding Term] -> Args
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Term -> Arg Term
forall a. WithHiding a -> Arg a
mkWithArg [WithHiding Term]
withArgs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
us2
        -- Andreas, 2013-02-26 add with-name to signature for printing purposes
        QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
aux Type
HasCallStack => Type
__DUMMY_TYPE__ Defn
emptyFunction

        -- Andreas, 2013-02-26 separate msgs to see which goes wrong
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          let ([Term]
vs, [EqualityView]
as) = (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> [WithHiding (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing [WithHiding (Term, EqualityView)]
vtys in
          [ TCM Doc
"    with arguments" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Term -> TCM Doc) -> [Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs)
          , TCM Doc
"             types" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((EqualityView -> TCM Doc) -> [EqualityView] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map EqualityView -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [EqualityView]
as)
          , TCM Doc
"with function call" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
          , TCM Doc
"           context" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Tele (Dom Type) -> TCM Doc)
-> TCMT IO (Tele (Dom Type)) -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)
          , TCM Doc
"             delta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta
          , TCM Doc
"            delta1" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta1
          , TCM Doc
"            delta2" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta2
          , TCM Doc
"              body" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
          ]

        (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v, QName
-> QName
-> Type
-> Tele (Dom Type)
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [WithHiding (Term, EqualityView)]
-> Type
-> NAPs
-> VerboseLevel
-> Permutation
-> Permutation
-> Permutation
-> [Clause]
-> WithFunctionProblem
WithFunction QName
x QName
aux Type
t Tele (Dom Type)
delta Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 [WithHiding (Term, EqualityView)]
vtys Type
t' NAPs
ps VerboseLevel
npars Permutation
perm' Permutation
perm Permutation
finalPerm [Clause]
cs)

-- | Invoked in empty context.
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction [Name]
_ WithFunctionProblem
NoWithFunction = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkWithFunction [Name]
cxtNames (WithFunction QName
f QName
aux Type
t Tele (Dom Type)
delta Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 [WithHiding (Term, EqualityView)]
vtys Type
b NAPs
qs VerboseLevel
npars Permutation
perm' Permutation
perm Permutation
finalPerm [Clause]
cs) = do

  let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
      withSub :: Substitution
      withSub :: Substitution
withSub = let as :: [EqualityView]
as = (WithHiding (Term, EqualityView) -> EqualityView)
-> [WithHiding (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> WithHiding (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing) [WithHiding (Term, EqualityView)]
vtys in
                VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta2) (VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
wkS ([EqualityView] -> VerboseLevel
countWithArgs [EqualityView]
as) Substitution
forall a. Substitution' a
idS)
                Substitution -> Substitution -> Substitution
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Empty -> Permutation -> Substitution
forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Permutation -> Permutation
reverseP Permutation
perm')

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"checkWithFunction"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      let ([Term]
vs, [EqualityView]
as) = (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> [WithHiding (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing [WithHiding (Term, EqualityView)]
vtys in
      [ TCM Doc
"delta1 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta1
      , TCM Doc
"delta2 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta2)
      , TCM Doc
"t      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      , TCM Doc
"as     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 ([EqualityView] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [EqualityView]
as)
      , TCM Doc
"vs     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs
      , TCM Doc
"b      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
      , TCM Doc
"qs     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCM Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
qs
      , TCM Doc
"perm'  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm')
      , TCM Doc
"perm   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm)
      , TCM Doc
"fperm  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
finalPerm)
      , TCM Doc
"withSub=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Substitution -> VerboseKey
forall a. Show a => a -> VerboseKey
show Substitution
withSub)
      ]
    ]

  -- Add the type of the auxiliary function to the signature

  -- Generate the type of the with function
  Tele (Dom Type)
delta1 <- Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
delta1 -- Issue 1332: checkInternal is picky about argInfo
                             -- but module application is sloppy.
                             -- We normalise to get rid of Def's coming
                             -- from module applications.
  (Type
withFunType, VerboseLevel
n) <- Tele (Dom Type)
-> [WithHiding (Term, EqualityView)]
-> Tele (Dom Type)
-> Type
-> TCM (Type, VerboseLevel)
withFunctionType Tele (Dom Type)
delta1 [WithHiding (Term, EqualityView)]
vtys Tele (Dom Type)
delta2 Type
b
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.type" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"with-function type:", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
withFunType ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.type" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"with-function type:", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Type
withFunType ]

  -- Andreas, 2013-10-21
  -- Check generated type directly in internal syntax.
  [Clause] -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange [Clause]
cs (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall Call
NoHighlighting (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$   -- To avoid flicker.
    Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Type -> Call
CheckWithFunctionType Type
withFunType) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Type -> TCM ()
forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
withFunType

  -- With display forms are closed
  Open DisplayForm
df <- TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm))
-> TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm)
forall a b. (a -> b) -> a -> b
$ DisplayForm -> TCMT IO (Open DisplayForm)
forall (m :: * -> *) a. MonadTCEnv m => a -> m (Open a)
makeOpen (DisplayForm -> TCMT IO (Open DisplayForm))
-> TCMT IO DisplayForm -> TCMT IO (Open DisplayForm)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName
-> QName
-> Tele (Dom Type)
-> Tele (Dom Type)
-> VerboseLevel
-> NAPs
-> Permutation
-> Permutation
-> TCMT IO DisplayForm
withDisplayForm QName
f QName
aux Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 VerboseLevel
n NAPs
qs Permutation
perm' Permutation
perm

  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.with.top" VerboseLevel
20 VerboseKey
"created with display form"

  case Open DisplayForm -> DisplayForm
forall (t :: * -> *) a. Decoration t => t a -> a
dget Open DisplayForm
df of
    Display VerboseLevel
n Elims
ts DisplayTerm
dt ->
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Display" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
        [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n)
        , [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> TCM Doc) -> Elims -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
ts
        , DisplayTerm -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DisplayTerm
dt
        ]
  QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
aux Type
withFunType Defn
emptyFunction)
                   { defDisplay :: [Open DisplayForm]
defDisplay = [Open DisplayForm
df] }
  -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"added with function" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
aux) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"of type"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
withFunType
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-|" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Tele (Dom Type) -> TCM Doc)
-> TCMT IO (Tele (Dom Type)) -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)
    ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.top" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"raw with func. type = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show Type
withFunType
    ]


  -- Construct the body for the with function
  [Clause' SpineLHS]
cs <- [Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS])
-> [Clause' SpineLHS] -> TCMT IO [Clause' SpineLHS]
forall a b. (a -> b) -> a -> b
$ (Clause -> Clause' SpineLHS) -> [Clause] -> [Clause' SpineLHS]
forall a b. (a -> b) -> [a] -> [b]
map (Clause -> Clause' SpineLHS
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine) [Clause]
cs
  [Clause' SpineLHS]
cs <- [Name]
-> QName
-> QName
-> Type
-> Tele (Dom Type)
-> NAPs
-> VerboseLevel
-> Substitution
-> Permutation
-> VerboseLevel
-> VerboseLevel
-> [Clause' SpineLHS]
-> TCMT IO [Clause' SpineLHS]
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Tele (Dom Type)
delta NAPs
qs VerboseLevel
npars Substitution
withSub Permutation
finalPerm (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
delta1) VerboseLevel
n [Clause' SpineLHS]
cs
  [Clause]
cs <- [Clause] -> TCMT IO [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> TCMT IO [Clause]) -> [Clause] -> TCMT IO [Clause]
forall a b. (a -> b) -> a -> b
$ (Clause' SpineLHS -> Clause) -> [Clause' SpineLHS] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map (Clause' SpineLHS -> Clause
forall a b. LHSToSpine a b => b -> a
A.spineToLhs) [Clause' SpineLHS]
cs

  -- Check the with function
  Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe Substitution
-> [Clause]
-> TCM ()
checkFunDefS Type
withFunType ArgInfo
defaultArgInfo Delayed
NotDelayed Maybe ExtLamInfo
forall a. Maybe a
Nothing (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f) DefInfo
forall t. DefInfo' t
info QName
aux (Substitution -> Maybe Substitution
forall a. a -> Maybe a
Just Substitution
withSub) [Clause]
cs

  where
    info :: DefInfo' t
info = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
Info.mkDefInfo (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
aux) Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef ([Clause] -> Range
forall t. HasRange t => t -> Range
getRange [Clause]
cs)

-- | Type check a where clause.
checkWhere
  :: A.WhereDeclarations -- ^ Where-declarations to check.
  -> TCM a               -- ^ Continuation.
  -> TCM a
checkWhere :: WhereDeclarations -> TCM a -> TCM a
checkWhere wh :: WhereDeclarations
wh@(A.WhereDecls Maybe ModuleName
whmod [Declaration]
ds) TCM a
ret = do
  Maybe ModuleName -> TCM ()
forall (m :: * -> *).
(MonadTCM m, MonadError TCErr m, MonadReduce m, MonadAddContext m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames m, IsString (m Doc),
 Null (m Doc), Semigroup (m Doc)) =>
Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
whmod
  [Declaration] -> TCM a
loop [Declaration]
ds
  where
    loop :: [Declaration] -> TCM a
loop [Declaration]
ds = case [Declaration]
ds of
      [] -> TCM a
ret
      [A.ScopedDecl ScopeInfo
scope [Declaration]
ds] -> ScopeInfo -> TCM a -> TCM a
forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
scope (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ [Declaration] -> TCM a
loop [Declaration]
ds
      [A.Section ModuleInfo
_ ModuleName
m GeneralizeTelescope
tel [Declaration]
ds]  -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection ModuleName
m GeneralizeTelescope
tel (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
          (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCheckingWhere :: Bool
envCheckingWhere = Bool
True }) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
            [Declaration] -> TCM ()
checkDecls [Declaration]
ds
            TCM a
ret
      [Declaration]
_ -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- #2897: We can't handle named where-modules in refined contexts.
    ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
Nothing = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    ensureNoNamedWhereInRefinedContext (Just ModuleName
m) = Call -> m () -> m ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (ModuleName -> Call
CheckNamedWhere ModuleName
m) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      [Term]
args <- (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> m Args -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> m Args
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m Args
moduleParamsToApply (ModuleName -> m Args) -> m ModuleName -> m Args
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Term] -> Bool
isWeakening [Term]
args) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ -- weakened contexts are fine
        Doc -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> m ()) -> m Doc -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          [VerboseKey]
names <- (Dom (VerboseKey, Type) -> VerboseKey)
-> [Dom (VerboseKey, Type)] -> [VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> VerboseKey
argNameToString (VerboseKey -> VerboseKey)
-> (Dom (VerboseKey, Type) -> VerboseKey)
-> Dom (VerboseKey, Type)
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst ((VerboseKey, Type) -> VerboseKey)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Type))
-> Dom (VerboseKey, Type)
-> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (VerboseKey, Type)] -> [VerboseKey])
-> (Tele (Dom Type) -> [Dom (VerboseKey, Type)])
-> Tele (Dom Type)
-> [VerboseKey]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList (Tele (Dom Type) -> [VerboseKey])
-> m (Tele (Dom Type)) -> m [VerboseKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                    (ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (ModuleName -> m (Tele (Dom Type)))
-> m ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
          let pr :: VerboseKey -> a -> m Doc
pr VerboseKey
x a
v = VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" =") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
          [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords (VerboseKey -> [m Doc]) -> VerboseKey -> [m Doc]
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Named where-modules are not allowed when module parameters have been refined by pattern matching. " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                             VerboseKey
"See https://github.com/agda/agda/issues/2897.")
            , VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> m Doc) -> VerboseKey -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"In this case the module parameter" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                     (if [Term] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Term]
args VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then VerboseKey
"s have" else VerboseKey
" has") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                     VerboseKey
" been refined to"
            , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((VerboseKey -> Term -> m Doc) -> [VerboseKey] -> [Term] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseKey -> Term -> m Doc
forall (m :: * -> *) a.
(PrettyTCM a, MonadReduce m, MonadAddContext m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames m, IsString (m Doc),
 Null (m Doc), Semigroup (m Doc)) =>
VerboseKey -> a -> m Doc
pr [VerboseKey]
names [Term]
args) ]
      where
        isWeakening :: [Term] -> Bool
isWeakening [] = Bool
True
        isWeakening (Var VerboseLevel
i [] : [Term]
args) = VerboseLevel -> [Term] -> Bool
isWk (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) [Term]
args
          where
            isWk :: VerboseLevel -> [Term] -> Bool
isWk VerboseLevel
i []                = Bool
True
            isWk VerboseLevel
i (Var VerboseLevel
j [] : [Term]
args) = VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j Bool -> Bool -> Bool
&& VerboseLevel -> [Term] -> Bool
isWk (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) [Term]
args
            isWk VerboseLevel
_ [Term]
_ = Bool
False
        isWeakening [Term]
_ = Bool
False


-- | Enter a new section during type-checking.

newSection :: ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
newSection :: ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection ModuleName
m gtel :: GeneralizeTelescope
gtel@(A.GeneralizeTel Map QName Name
_ Telescope
tel) TCM a
cont = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.section" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"checking section" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((TypedBinding -> TCM Doc) -> Telescope -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Telescope
tel)

  GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
forall a.
GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
checkGeneralizeTelescope GeneralizeTelescope
gtel (([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a)
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ [Maybe Name]
_ Tele (Dom Type)
tel' -> do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.section" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"adding section:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
tel'))

    ModuleName -> TCM ()
addSection ModuleName
m

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.section" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
4 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"actual tele:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Tele (Dom Type) -> TCM Doc)
-> TCMT IO (Tele (Dom Type)) -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m

    ModuleName -> TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m TCM a
cont

-- | Set the current clause number.

atClause :: QName -> Int -> Type -> Maybe Substitution -> A.SpineClause -> TCM a -> TCM a
atClause :: QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> TCM a
-> TCM a
atClause QName
name VerboseLevel
i Type
t Maybe Substitution
sub Clause' SpineLHS
cl TCM a
ret = do
  Closure ()
clo <- () -> TCMT IO (Closure ())
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure ()
  (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envClause :: IPClause
envClause = QName
-> VerboseLevel
-> Type
-> Maybe Substitution
-> Clause' SpineLHS
-> Closure ()
-> [Closure IPBoundary]
-> IPClause
IPClause QName
name VerboseLevel
i Type
t Maybe Substitution
sub Clause' SpineLHS
cl Closure ()
clo [] }) TCM a
ret