{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Def where

import Prelude hiding ( null )

import Control.Monad        ( forM, forM_ )
import Control.Monad.Except ( MonadError(..) )

import Data.Bifunctor
import Data.Function (on)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Semigroup ( sconcat )

import Agda.Interaction.Options

import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Pretty 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 Agda.Syntax.Internal.MetaVars (allMetasList)
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Info hiding (defAbstract)

import Agda.TypeChecking.Monad
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.Telescope.Path
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.CompiledClause (CompiledClauses', pattern Done, hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.RecordPatterns ( recordRHSToCopatterns )
import Agda.TypeChecking.Sort

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

import Agda.Utils.Function ( applyWhen, applyWhenM )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty ( prettyShow )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Update

import Agda.Utils.Impossible
import Agda.Utils.Tuple (snd3, fst3)

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

checkFunDef :: A.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef :: DefInfo' Expr -> QName -> [Clause] -> TCM ()
checkFunDef DefInfo' Expr
i QName
name [Clause]
cs = do
        -- Reset blocking tag (in case a previous attempt was blocked)
        (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
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' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
name) ()
        -- Get the type and relevance of the function
        def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, ReadTCState 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
name
        let t    = Definition -> Type'' Term Term
defType Definition
def
        let info = Definition -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Definition
def

        -- If the function is erased, then hard compile-time mode is
        -- entered.
        setHardCompileTimeModeIfErased' info $ do

        case isAlias cs t of  -- #418: Don't use checkAlias for abstract definitions, since the type
                              -- of an abstract function must not be informed by its definition.
          Just (Expr
e, Maybe Expr
mc, MetaId
x)
            | DefInfo' Expr -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo' Expr
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef, DefInfo' Expr -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo' Expr
i IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef ->
              Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range' SrcFile -> QName -> Bool -> Call
CheckFunDefCall (DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
i) QName
name Bool
True) (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.
                -- Ulf, 2021-02-09: also unfreeze metas in the sort of this type
                TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                  xs <- Type'' Term Term -> [MetaId]
forall a. AllMetas a => a -> [MetaId]
allMetasList (Type'' Term Term -> [MetaId])
-> (MetaVariable -> Type'' Term Term) -> MetaVariable -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> (MetaVariable -> Judgement MetaId)
-> MetaVariable
-> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> [MetaId])
-> TCMT IO MetaVariable -> TCMT IO [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
                  mapM_ unfreezeMeta (x : xs)
                Type'' Term Term
-> ArgInfo
-> DefInfo' Expr
-> QName
-> Expr
-> Maybe Expr
-> TCM ()
checkAlias Type'' Term Term
t ArgInfo
info DefInfo' Expr
i QName
name Expr
e Maybe Expr
mc
            | Bool
otherwise -> do -- Warn about abstract alias (will never work!)
              -- Ulf, 2021-11-18, #5620: Don't warn if the meta is solved. A more intuitive solution
              -- would be to not treat definitions with solved meta types as aliases, but in mutual
              -- blocks you might actually have solved the type of an alias by the time you get to
              -- the definition. See test/Succeed/SizeInfinity.agda for an example where this
              -- happens.
              TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool)
-> TCMT IO MetaInstantiation -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
                DefInfo' Expr -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange DefInfo' Expr
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IsOpaque -> Warning
MissingTypeSignatureForOpaque QName
name (DefInfo' Expr -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo' Expr
i)
              Type'' Term Term
-> ArgInfo
-> Maybe ExtLamInfo
-> DefInfo' Expr
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type'' Term Term
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing DefInfo' Expr
i QName
name [Clause]
cs
          Maybe (Expr, Maybe Expr, MetaId)
_ -> Type'' Term Term
-> ArgInfo
-> Maybe ExtLamInfo
-> DefInfo' Expr
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type'' Term Term
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing DefInfo' Expr
i QName
name [Clause]
cs

        -- If it's a macro check that it ends in Term → TC ⊤
        let 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
        when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
    TCM () -> ((TCErr, Blocker) -> TCM ()) -> TCM ()
forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, Blocker
blocker) -> do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
          [ TCMT IO Doc
"checking function definition got stuck on: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
blocker ]
        (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
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
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
        Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefInfo' Expr -> QName -> [Clause] -> TCErr -> Constraint
CheckFunDef DefInfo' Expr
i QName
name [Clause]
cs TCErr
err

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

  let telList = Tele (Dom (Type'' Term Term)) -> [Dom ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom (Type'' Term Term))
tel
      resType = Tele (Dom (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
abstract ([Dom ([Char], Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList (Int
-> [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
forall a. Int -> [a] -> [a]
drop ([Dom ([Char], Type'' Term Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type'' Term Term)]
telList Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Dom ([Char], Type'' Term Term)]
telList)) Type'' Term Term
tr
  expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
  equalType resType expectedType
    `catchError` \ TCErr
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
MacroResultTypeMismatch Type'' Term Term
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'' Term Term -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause]
cs Type'' Term Term
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 Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
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) WhereDeclarations
wh Catchall
_]
      | WhereDeclarations -> Bool
forall a. Null a => a -> Bool
null WhereDeclarations
wh     = (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 -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias :: Type'' Term Term
-> ArgInfo
-> DefInfo' Expr
-> QName
-> Expr
-> Maybe Expr
-> TCM ()
checkAlias Type'' Term Term
t ArgInfo
ai DefInfo' Expr
i QName
name Expr
e Maybe Expr
mc =
  let clause :: SpineClause
clause = A.Clause { clauseLHS :: SpineLHS
clauseLHS          = LHSInfo -> QName -> [NamedArg (Pattern' Expr)] -> SpineLHS
A.SpineLHS (Range' SrcFile -> ExpandedEllipsis -> LHSInfo
LHSInfo (DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
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 :: Catchall
clauseCatchall     = Catchall
forall a. Null a => a
empty } in
  QName
-> Int
-> Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> TCM ()
-> TCM ()
forall a.
QName
-> Int
-> Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
0 Type'' Term Term
t IsWithFunction (Substitution' Term)
forall a. IsWithFunction a
NoWithFunction SpineClause
clause (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.alias" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkAlias" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon  TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
    , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
equals TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> 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.
  v <- ArgInfo -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r, ExpandCase (tcm a)) =>
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'' Term Term -> TCMT IO Term
checkDontExpandLast Comparison
CmpLeq Expr
e Type'' Term Term
t

  reportSDoc "tc.def.alias" 20 $ "checkAlias: finished checking"

  solveSizeConstraints DontDefaultToInfty

  v <- instantiateFull 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 = Bool -> (Term -> Term) -> Term -> Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
ai) Term -> Term
dontCare

  -- Add the definition
  fun <- emptyFunctionData
  addConstant' name ai t $ FunctionDefn $
    set funMacro_ (Info.defMacro i == MacroDef) $
    set funAbstr_ (Info.defAbstract i) $
      fun { _funClauses   = [ Clause  -- trivial clause @name = v@
              { clauseLHSRange    = getRange i
              , clauseFullRange   = getRange i
              , clauseTel         = EmptyTel
              , namedClausePats   = []
              , clauseBody        = Just $ bodyMod v
              , clauseType        = Just $ Arg ai t
              , clauseCatchall    = empty
              , clauseRecursive   = MaybeRecursive   -- we don't know yet
              , clauseUnreachable = Just False
              , clauseEllipsis    = NoEllipsis
              , clauseWhereModule = Nothing
              } ]
          , _funCompiled  = Just $ Done 0 MaybeRecursive [] $ bodyMod v
          , _funSplitTree = Just $ SplittingDone 0
          , _funOpaque    = Info.defOpaque i
          }

  -- Andreas, 2017-01-01, issue #2372:
  -- Add the definition to the instance table, if needed, to update its type.
  case Info.defInstance i of
    InstanceDef KwRange
kwr -> QName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
name (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ KwRange -> QName -> Type'' Term Term -> TCM ()
readdTypedInstance KwRange
kwr QName
name Type'' Term Term
t
      -- Put highlighting on the name only;
      -- @(getRange (r, name))@ does not give good results.
    IsInstance
NotInstanceDef -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  reportSDoc "tc.def.alias" 20 $ "checkAlias: leaving"


-- | Type check a definition by pattern matching.
checkFunDef' ::
     Type             -- ^ The type we expect the function to have.
  -> ArgInfo          -- ^ Is it irrelevant or erased etc.?
  -> Maybe ExtLamInfo -- ^ Does the definition come from an extended lambda?
                      --   If so, we need to know some stuff about lambda-lifted args.
  -> A.DefInfo        -- ^ 'Range' info.
  -> QName            -- ^ The name of the function.
  -> [A.Clause]       -- ^ The clauses to check.
  -> TCM ()
checkFunDef' :: Type'' Term Term
-> ArgInfo
-> Maybe ExtLamInfo
-> DefInfo' Expr
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type'' Term Term
t ArgInfo
ai Maybe ExtLamInfo
extlam DefInfo' Expr
i QName
name [Clause]
cs =
  Type'' Term Term
-> ArgInfo
-> Maybe ExtLamInfo
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> DefInfo' Expr
-> QName
-> [Clause]
-> TCM ()
checkFunDefS Type'' Term Term
t ArgInfo
ai Maybe ExtLamInfo
extlam IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
forall a. IsWithFunction a
NoWithFunction DefInfo' Expr
i QName
name [Clause]
cs

-- | Type check a definition by pattern matching.
checkFunDefS ::
     Type             -- ^ The type we expect the function to have.
  -> ArgInfo          -- ^ Is it irrelevant or erased etc.?
  -> Maybe ExtLamInfo -- ^ Does the definition come from an extended lambda?
                      --   If so, we need to know some stuff about lambda-lifted args.
  -> IsWithFunction (QName, Substitution, Map Name LetBinding)
       -- ^ Is it a with function (if so, what's the name of the parent function)?
       -- ^ In that case, also substitution (from with abstraction) that needs to be applied
       --   to module parameters, and let-bindings inherited from parent clause.
  -> A.DefInfo        -- ^ 'Range' info.
  -> QName            -- ^ The name of the function.
  -> [A.Clause]       -- ^ The clauses to check.
  -> TCM ()
checkFunDefS :: Type'' Term Term
-> ArgInfo
-> Maybe ExtLamInfo
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> DefInfo' Expr
-> QName
-> [Clause]
-> TCM ()
checkFunDefS Type'' Term Term
t ArgInfo
ai Maybe ExtLamInfo
extlam IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
with DefInfo' Expr
i QName
name [Clause]
cs = do

    Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range' SrcFile -> QName -> Bool -> Call
CheckFunDefCall (DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
i) QName
name Bool
True) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.fun" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking body of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"full type:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM (Type'' Term Term -> TCMT IO Doc)
-> (Definition -> Type'' Term Term) -> Definition -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type'' Term Term
defType (Definition -> TCMT IO Doc) -> TCMT IO Definition -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
name)
              ]

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.fun" Int
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (Clause -> TCMT IO Doc) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Clause -> [Char]) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Char]
forall a. Show a => a -> [Char]
show (Clause -> [Char]) -> (Clause -> Clause) -> Clause -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Clause
forall a. ExprLike a => a -> a
A.deepUnscope) [Clause]
cs

        cs <- [SpineClause] -> TCMT IO [SpineClause]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SpineClause] -> TCMT IO [SpineClause])
-> [SpineClause] -> TCMT IO [SpineClause]
forall a b. (a -> b) -> a -> b
$! (Clause -> SpineClause) -> [Clause] -> [SpineClause]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> SpineClause
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine [Clause]
cs

        reportSDoc "tc.def.fun" 70 $
          sep $ "spine clauses:" : fmap (nest 2 . text . show . A.deepUnscope) 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
        cs <- traceCall NoHighlighting $ do -- To avoid flicker.
          forM (zip' cs [0..]) $ \ (SpineClause
c, Int
clauseNo) -> do
            QName
-> Int
-> Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
QName
-> Int
-> Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
clauseNo Type'' Term Term
t ((QName, Substitution' Term, Map Name LetBinding)
-> Substitution' Term
forall a b c. (a, b, c) -> b
snd3 ((QName, Substitution' Term, Map Name LetBinding)
 -> Substitution' Term)
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> IsWithFunction (Substitution' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
with) SpineClause
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
              (c,b) <- ArgInfo
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r, ExpandCase (tcm a)) =>
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'' Term Term
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type'' Term Term
t IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
with SpineClause
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.
              whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
              -- Andreas, 2013-10-27 add clause as soon it is type-checked
              -- TODO: instantiateFull?
              inTopContext $ addClauses name [c]
              return (c,b)

        (cs, CPC isOneIxs) <- return $! (second mconcat . unzip) cs

        -- If there is a partial match ("system"), no proper (co)pattern matching is allowed.
        let 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
        when isSystem do
          -- allow VarP and ConP i0/i1 fallThrough = yes, DotP
          let pss = (Clause -> [NamedArg DeBruijnPattern])
-> [Clause] -> [[NamedArg DeBruijnPattern]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> [NamedArg DeBruijnPattern]
namedClausePats [Clause]
cs
              allowed = \case
                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
          unless (all (all $ allowed . namedArg) pss) $
            typeError PatternInSystem

        reportSDoc "tc.def.fun" 70 $ inTopContext $ do
          sep $ "checked clauses:" : fmap (nest 2 . text . show) cs

        reportSDoc "tc.cc" 25 $ inTopContext $ do
          sep [ "clauses before injectivity test"
              , nest 2 $ prettyTCM $ fmap (QNamed name) cs  -- broken, reify (QNamed n cl) expect cl to live at top level
              ]
        reportSDoc "tc.cc" 90 $ inTopContext $ do
          sep [ "raw clauses: "
              , nest 2 $ sep $ fmap (text . show . QNamed name) cs
              ]

        -- Needed to calculate the proper fullType below.
        applyWhenM (optPolarity <$> pragmaOptions) (applyPolarityToContext ai) $
          applyCohesionToContext ai $ do

        -- Systems have their own coverage and "coherence" check, we
        -- also add an absurd clause for the cases not needed.
        (cs,sys) <- if not isSystem then return (cs, empty) else do
                 fullType <- flip abstract t <$> getContextTelescope
                 sys <- inTopContext $ checkSystemCoverage name (IntSet.toList isOneIxs) fullType cs
                 tel <- getContextTelescope
                 let c = Clause
                       { clauseFullRange :: Range' SrcFile
clauseFullRange = Range' SrcFile
forall a. Range' a
noRange
                       , clauseLHSRange :: Range' SrcFile
clauseLHSRange  = Range' SrcFile
forall a. Range' a
noRange
                       , clauseTel :: Tele (Dom (Type'' Term Term))
clauseTel       = Tele (Dom (Type'' Term Term))
tel
                       , namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = Tele (Dom (Type'' Term Term)) -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom (Type'' Term Term))
tel
                       , clauseBody :: Maybe Term
clauseBody      = Maybe Term
forall a. Maybe a
Nothing
                       , clauseType :: Maybe (Arg (Type'' Term Term))
clauseType      = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Type'' Term Term -> Arg (Type'' Term Term)
forall a. a -> Arg a
defaultArg Type'' Term Term
t)
                       , clauseCatchall :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
                       , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive
                       , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                       , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                       , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                       }
                 return (cs ++! [c], pure sys)

        -- The macro or inline tags might be on the type signature
        info <- getConstInfo name
        let
          ismacro  = Defn -> Bool
isMacro (Definition -> Defn
theDef Definition
info)
          isinline = Defn -> Bool
isInlineFun (Definition -> Defn
theDef Definition
info)

        -- Annotate the clauses with which arguments are actually used.
        cs <- instantiateFull {- =<< mapM rebindClause -} 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!?

        -- Inline copattern record constructors on demand, unless the
        -- function is marked inline.
        cs <- if isinline then pure cs else concat <$> do
          forM cs $ \ Clause
cl -> do
            (cls, nonExactSplit) <- ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool))
-> ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
forall a b. (a -> b) -> a -> b
$ Clause -> ChangeT (TCMT IO) [Clause]
forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns Clause
cl
            when nonExactSplit do
              -- If we inlined a non-eta constructor, issue a warning
              -- (pointing at the clause lhs) that the clause does not
              -- hold as definitional equality.
              setCurrentRange (clauseLHSRange cl) . warning $ InlineNoExactSplit name cl
            return cls

        -- After checking, remove the clauses again.
        -- (Otherwise, @checkInjectivity@ loops for issue 801).
        --
        -- Amy, 2025-04-03: We can't remove the clauses before doing
        -- record→copattern translation, since we might need the
        -- previous clauses to come up with the types of the projected
        -- fields; see 'test/Succeed/IApplyRecConstrInline'.
        modifyFunClauses name (const [])

        -- 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.
        reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
        inv <- Bench.billTo [Bench.Injectivity] $
          checkInjectivity name cs

        reportSDoc "tc.cc" 15 $ inTopContext $ do
          sep [ "clauses before compilation"
              , nest 2 $ sep $ fmap (prettyTCM . QNamed name) cs
              ]

        reportSDoc "tc.cc.raw" 65 $ do
          sep [ "clauses before compilation"
              , nest 2 $ sep $ fmap (text . show) cs
              ]

        -- add clauses for the coverage (& confluence) checker (needs to reduce)
        inTopContext $ addClauses name cs

        reportSDoc "tc.cc.type" 60 $ "  type   : " <+> (text . prettyShow) t
        reportSDoc "tc.cc.type" 60 $ "  context: " <+> (text . prettyShow =<< getContextTelescope)

        fullType <- flip telePi t <$> getContextTelescope

        reportSLn  "tc.cc.type" 80 $ show fullType

        -- Coverage check and compile the clauses
        (mst, _recordExpressionBecameCopatternLHS, cc) <- Bench.billTo [Bench.Coverage] $
          unsafeInTopContext $ compileClauses (if isSystem then Nothing else (Just (name, fullType)))
                                        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.
        cs <- defClauses <$> getConstInfo name

        reportSDoc "tc.cc" 60 $ inTopContext $ do
          sep [ "compiled clauses of" <+> prettyTCM name
              , nest 2 $ pretty cc
              ]

        covering <- funCovering . theDef <$> getConstInfo name

        -- Add the definition
        inTopContext $ addConstant name =<< do

          reportSDoc "tc.def.fun.clauses" 15 $ inTopContext $ do
            vcat [ "final clauses for" <+> prettyTCM name <+>  ":"
                 , nest 2 $ vcat $ map' (prettyTCM . QNamed name) cs
                 ]

          -- If there was a pragma for this definition, we can set the
          -- funTerminates field directly.
          --
          -- Amy, 2025-04-03: If the function was marked INLINE before
          -- the clauses were checked the result should also be INLINE.
          fun  <- emptyFunctionData
          defn <- autoInline $ set funInline isinline $ FunctionDefn $
           set funMacro_ (ismacro || Info.defMacro i == MacroDef) $
           set funAbstr_ (Info.defAbstract i) $
           fun
             { _funClauses        = cs
             , _funCompiled       = Just cc
             , _funSplitTree      = mst
             , _funInv            = inv
             , _funOpaque         = Info.defOpaque i
             , _funExtLam         = (\ ExtLamInfo
e -> ExtLamInfo
e { extLamSys = sys }) <$> extlam
             , _funWith           = fmap fst3 with
             , _funCovering       = covering
             }
          lang <- getLanguage
          useTerPragma $
            updateDefCopatternLHS (const $ hasProjectionPatterns cc) $
            (defaultDefn ai name fullType lang defn)

        reportSDoc "tc.def.fun" 10 $ do
          sep [ "added " <+> prettyTCM name <+> ":"
              , nest 2 $ prettyTCM . defType =<< getConstInfo name
              ]

        -- Jesper, 2019-05-30: if the constructors used in the
        -- lhs of a clause have rewrite rules, we need to check
        -- confluence here
        whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
confChk -> 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
$
          ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses ConfluenceCheck
confChk 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
  tc <- Lens' TCEnv (TerminationCheck ()) -> TCMT IO (TerminationCheck ())
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (TerminationCheck () -> f (TerminationCheck ()))
-> TCEnv -> f TCEnv
Lens' TCEnv (TerminationCheck ())
eTerminationCheck
  let 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
  reportS "tc.fundef" 30 $
    [ "funTerminates of " ++! prettyShow name ++! " set to " ++! show terminates
    , "  tc = " ++! show tc
    ]
  return $! def { theDef = fun { funTerminates = terminates }}
useTerPragma Definition
def = Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def

-- | Modify all the @LHSCore@s of the given piece of syntax.
-- (Used to insert patterns for @rewrite@ or the inspect idiom)
class HasLHSCores a where
  mapLHSCores :: (A.LHSCore -> A.LHSCore) -> (a -> a)

instance HasLHSCores A.RHS where
  mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f = \case
    A.WithRHS QName
aux List1 WithExpr
es List1 Clause
cs -> QName -> List1 WithExpr -> List1 Clause -> RHS
A.WithRHS QName
aux List1 WithExpr
es (List1 Clause -> RHS) -> List1 Clause -> RHS
forall a b. (a -> b) -> a -> b
$ List1 Clause -> (Clause -> Clause) -> List1 Clause
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for List1 Clause
cs ((Clause -> Clause) -> List1 Clause)
-> (Clause -> Clause) -> List1 Clause
forall a b. (a -> b) -> a -> b
$ (LHSCore' Expr -> LHSCore' Expr) -> Clause -> Clause
forall a.
HasLHSCores a =>
(LHSCore' Expr -> LHSCore' Expr) -> a -> a
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f
    A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
forall a.
HasLHSCores a =>
(LHSCore' Expr -> LHSCore' Expr) -> a -> a
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f RHS
rhs) WhereDeclarations
wh
    rhs :: RHS
rhs@RHS
A.AbsurdRHS -> RHS
rhs
    rhs :: RHS
rhs@A.RHS{}     -> RHS
rhs

instance HasLHSCores A.LHS where
  mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> LHS -> LHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f (A.LHS LHSInfo
info LHSCore' Expr
core) = LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
info (LHSCore' Expr -> LHSCore' Expr
f LHSCore' Expr
core)

instance HasLHSCores A.Clause where
  mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> Clause -> Clause
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f (A.Clause LHS
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Catchall
catchall) =
    LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
A.Clause ((LHSCore' Expr -> LHSCore' Expr) -> LHS -> LHS
forall a.
HasLHSCores a =>
(LHSCore' Expr -> LHSCore' Expr) -> a -> a
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f LHS
lhs) [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
forall a.
HasLHSCores a =>
(LHSCore' Expr -> LHSCore' Expr) -> a -> a
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f RHS
rhs) WhereDeclarations
ds Catchall
catchall

-- | Insert some names into the with-clauses LHS of the given RHS.
-- (Used for the inspect idiom)
insertInspects :: List1 (Arg (Maybe A.BindName)) -> A.LHSCore -> A.LHSCore
insertInspects :: List1 (Arg (Maybe BindName)) -> LHSCore' Expr -> LHSCore' Expr
insertInspects List1 (Arg (Maybe BindName))
ps = \case
  A.LHSWith LHSCore' Expr
core NonEmpty (Arg (Pattern' Expr))
wps [] ->
    let ps' :: NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
ps' = (Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
-> List1 (Arg (Maybe BindName))
-> NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
-> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr)))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
 -> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
-> (Maybe BindName -> Maybe (Arg (Pattern' Expr)))
-> Arg (Maybe BindName)
-> Arg (Maybe (Arg (Pattern' Expr)))
forall a b. (a -> b) -> a -> b
$ (BindName -> Arg (Pattern' Expr))
-> Maybe BindName -> Maybe (Arg (Pattern' Expr))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindName -> Arg (Pattern' Expr)
patOfName) List1 (Arg (Maybe BindName))
ps in
    LHSCore' Expr
-> NonEmpty (Arg (Pattern' Expr))
-> [NamedArg (Pattern' Expr)]
-> LHSCore' Expr
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
A.LHSWith LHSCore' Expr
core (NonEmpty (Arg (Pattern' Expr))
-> [Arg (Pattern' Expr)] -> NonEmpty (Arg (Pattern' Expr))
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe NonEmpty (Arg (Pattern' Expr))
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Arg (Pattern' Expr)] -> NonEmpty (Arg (Pattern' Expr)))
-> [Arg (Pattern' Expr)] -> NonEmpty (Arg (Pattern' Expr))
forall a b. (a -> b) -> a -> b
$ [Arg (Maybe (Arg (Pattern' Expr)))]
-> [Arg (Pattern' Expr)] -> [Arg (Pattern' Expr)]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn (NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
-> [Item (NonEmpty (Arg (Maybe (Arg (Pattern' Expr)))))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
ps') (NonEmpty (Arg (Pattern' Expr))
-> [Item (NonEmpty (Arg (Pattern' Expr)))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (Arg (Pattern' Expr))
wps)) []
  -- Andreas, AIM XXXV, 2022-05-09, issue #5728:
  -- Cases other than LHSWith actually do not make sense, but let them
  -- through to get a proper error later.
  LHSCore' Expr
lhs -> LHSCore' Expr
lhs

  where

    patOfName :: A.BindName -> Arg A.Pattern
    patOfName :: BindName -> Arg (Pattern' Expr)
patOfName = Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
-> (BindName -> Pattern' Expr) -> BindName -> Arg (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP

    insertIn :: [Arg (Maybe (Arg a))]
             -> [Arg a] -> [Arg a]
    insertIn :: forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn []                 [Arg a]
wps  = [Arg a]
wps
    insertIn (Arg ArgInfo
info Maybe (Arg a)
nm : [Arg (Maybe (Arg a))]
ps) (Arg a
w : [Arg a]
wps) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info =
      Arg a
w Arg a -> [Arg a] -> [Arg a]
forall a. a -> [a] -> [a]
: Maybe (Arg a) -> [Arg a]
forall a. Maybe a -> [a]
maybeToList Maybe (Arg a)
nm [Arg a] -> [Arg a] -> [Arg a]
forall a. [a] -> [a] -> [a]
++! [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg a))]
ps [Arg a]
wps
    insertIn (Arg ArgInfo
info Maybe (Arg a)
nm : [Arg (Maybe (Arg a))]
ps) [Arg a]
wps       | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info =
          Maybe (Arg a) -> [Arg a]
forall a. Maybe a -> [a]
maybeToList Maybe (Arg a)
nm [Arg a] -> [Arg a] -> [Arg a]
forall a. [a] -> [a] -> [a]
++! [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg a))]
ps [Arg a]
wps
    insertIn [Arg (Maybe (Arg a))]
_ [Arg a]
_ = [Arg a]
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | Insert some with-patterns into the with-clauses LHS of the given RHS.
-- (Used for @rewrite@)
insertPatterns :: List1 (Arg A.Pattern) -> A.RHS -> A.RHS
insertPatterns :: NonEmpty (Arg (Pattern' Expr)) -> RHS -> RHS
insertPatterns NonEmpty (Arg (Pattern' Expr))
pats = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
forall a.
HasLHSCores a =>
(LHSCore' Expr -> LHSCore' Expr) -> a -> a
mapLHSCores (NonEmpty (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore NonEmpty (Arg (Pattern' Expr))
pats)

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

-- | Parameters for creating a @with@-function.
type WithFunctionProblem = IsWithFunction WithFunctionProblemData

data WithFunctionProblemData = WithFunctionProblemData
    { WithFunctionProblemData -> QName
wfParentName   :: QName                            -- ^ Parent function name.
    , WithFunctionProblemData -> QName
wfName         :: QName                            -- ^ With function name.
    , WithFunctionProblemData -> Type'' Term Term
wfParentType   :: Type                             -- ^ Type of the parent function.
    , WithFunctionProblemData -> Tele (Dom (Type'' Term Term))
wfParentTel    :: Telescope                        -- ^ Context of the parent patterns.
    , WithFunctionProblemData -> Tele (Dom (Type'' Term Term))
wfBeforeTel    :: Telescope                        -- ^ Types of arguments to the with function before the with expressions (needed vars).
    , WithFunctionProblemData -> Tele (Dom (Type'' Term Term))
wfAfterTel     :: Telescope                        -- ^ Types of arguments to the with function after the with expressions (unneeded vars).
    , WithFunctionProblemData -> NonEmpty (Arg (Term, EqualityView))
wfExprs        :: List1 (Arg (Term, EqualityView)) -- ^ With and rewrite expressions and their types.
    , WithFunctionProblemData -> Type'' Term Term
wfRHSType      :: Type                             -- ^ Type of the right hand side.
    , WithFunctionProblemData -> [NamedArg DeBruijnPattern]
wfParentPats   :: [NamedArg DeBruijnPattern]       -- ^ Parent patterns.
    , WithFunctionProblemData -> Int
wfParentParams :: Nat                              -- ^ Number of module parameters in parent patterns
    , WithFunctionProblemData -> Permutation
wfPermSplit    :: Permutation                      -- ^ Permutation resulting from splitting the telescope into needed and unneeded vars.
    , WithFunctionProblemData -> Permutation
wfPermParent   :: Permutation                      -- ^ Permutation reordering the variables in the parent pattern.
    , WithFunctionProblemData -> Permutation
wfPermFinal    :: Permutation                      -- ^ Final permutation (including permutation for the parent clause).
    , WithFunctionProblemData -> List1 Clause
wfClauses      :: List1 A.Clause                   -- ^ The given clauses for the with function
    , WithFunctionProblemData -> Substitution' Term
wfCallSubst    :: Substitution                     -- ^ Substitution to generate call for the parent.
    , WithFunctionProblemData -> Map Name LetBinding
wfLetBindings  :: Map Name LetBinding              -- ^ The let-bindings in scope of the parent (in the parent context).
    }

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

  case a of
    Def QName
q [Apply Arg Term
phi] -> do
      [iz,io] <- (BuiltinId -> TCMT IO (Maybe QName))
-> [BuiltinId] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' [BuiltinId
builtinIZero, BuiltinId
builtinIOne]
      ineg <- primINeg
      imin <- primIMin
      imax <- primIMax
      i0 <- primIZero
      i1 <- primIOne
      let
        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 DeBruijnPattern
_ = Maybe Bool
forall a. Maybe a
Nothing

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

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

        -- andI and orI have cases for singletons to improve error messages.
        andI, orI :: [Term] -> Term
        andI [] = Term
i1
        andI [Term
t] = Term
t
        andI (Term
t:[Term]
ts) = (\ Term
x -> Term
imin Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> 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
i0
        orI [Term
t] = Term
t
        orI (Term
t:[Term]
ts) = Term
imax Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> 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 = (Clause -> [DeBruijnPattern]) -> [Clause] -> [[DeBruijnPattern]]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> [DeBruijnPattern] -> [DeBruijnPattern]
forall a. Int -> [a] -> [a]
take' Int
n ([DeBruijnPattern] -> [DeBruijnPattern])
-> (Clause -> [DeBruijnPattern]) -> Clause -> [DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) ([NamedArg DeBruijnPattern] -> [DeBruijnPattern])
-> (Clause -> [NamedArg DeBruijnPattern])
-> Clause
-> [DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats) [Clause]
cs
        alphas :: [[(Int,Bool)]] -- the face maps corresponding to each clause
        alphas = ([DeBruijnPattern] -> [(Int, Bool)])
-> [[DeBruijnPattern]] -> [[(Int, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map' ([Int] -> [DeBruijnPattern] -> [(Int, Bool)]
collectDirs (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n)) [[DeBruijnPattern]]
pats
        phis :: [Term] -- the φ terms for each clause (i.e. the alphas as terms)
        phis = ([(Int, Bool)] -> Term) -> [[(Int, Bool)]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' ([Term] -> Term
andI ([Term] -> Term)
-> ([(Int, Bool)] -> [Term]) -> [(Int, Bool)] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Bool) -> Term) -> [(Int, Bool)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Bool) -> Term
dir)) [[(Int, Bool)]]
alphas
        psi = [Term] -> Term
orI ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
phis
        pcs = [Term] -> [Clause] -> [(Term, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip' [Term]
phis [Clause]
cs

      reportSDoc "tc.sys.cover" 20 $ fsep $ map' prettyTCM pats
      interval <- primIntervalType
      reportSDoc "tc.sys.cover" 10 $ "equalTerm " <+> prettyTCM (unArg phi) <+> prettyTCM psi
      equalTerm interval (unArg phi) psi

      forM_ (initWithDefault __IMPOSSIBLE__ $
             initWithDefault __IMPOSSIBLE__ $ List.tails pcs) $ \ ((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
          phi12 <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
imin Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
phi1, Term -> Arg Term
forall a. a -> Arg a
argN Term
phi2])
          forallFaceMaps phi12 (\ IntMap Bool
_ Blocker
_ -> Term -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__) $ \IntMap Bool
_ Substitution' Term
sigma -> do
            let args :: [Arg Term]
args = Substitution' Term
Substitution' (SubstArg [Arg Term])
sigma Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom (Type'' Term Term)) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom (Type'' Term Term))
gamma
                t' :: Type'' Term Term
t' = Substitution' Term
Substitution' (SubstArg (Type'' Term Term))
sigma Substitution' (SubstArg (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type'' Term Term
t
                fromReduced :: Reduced (Blocked' t yes) yes -> yes
fromReduced (YesReduction Simplification
_ yes
x) = yes
x
                fromReduced (NoReduction Blocked' t yes
x) = Blocked' t yes -> yes
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t yes
x
                body :: Clause -> TCMT IO Term
body Clause
cl = do
                  let extra :: Int
extra = [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop Int
n ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl)
                  TelV delta _ <- Int -> Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type'' Term Term -> m (TelV (Type'' Term Term))
telViewUpTo Int
extra Type'' Term Term
t'
                  fmap (abstract delta) $ addContext delta $ do
                    fmap fromReduced $ runReduceM $
                      appDef' f (Def f []) [cl] [] (map' notReduced $ raise (size delta) args ++! teleArgs delta)
            v1 <- Clause -> TCMT IO Term
body Clause
cl1
            v2 <- body cl2
            equalTerm t' v1 v2

      sys <- forM (zip' alphas cs) $ \ ([(Int, Bool)]
alpha,Clause
cl) -> do

            let
                -- Δ = Γ_α , Δ'α
                delta :: Tele (Dom (Type'' Term Term))
delta = Clause -> Tele (Dom (Type'' Term Term))
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 :: [NamedArg DeBruijnPattern]
ps = Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                extra :: Int
extra = [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [NamedArg DeBruijnPattern]
ps)
                -- size Δ'α = size Δ' = extra
                -- Γ , α ⊢ u
                takeLast :: Int -> [a] -> [a]
takeLast Int
n [a]
xs = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [a]
xs
                weak :: [Int] -> Substitution' a
weak [] = Substitution' a
forall a. Substitution' a
idS
                weak (Int
i:[Int]
is) = [Int] -> Substitution' a
weak [Int]
is Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i (Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS Int
1)
                tel :: Tele (Dom (Type'' Term Term))
tel = [Dom ([Char], Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList (Int
-> [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
forall a. Int -> [a] -> [a]
takeLast Int
extra (Tele (Dom (Type'' Term Term)) -> [Dom ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom (Type'' Term Term))
delta))
                u :: Term
u = Tele (Dom (Type'' Term Term)) -> Term -> Term
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
abstract Tele (Dom (Type'' Term Term))
tel (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
extra ([Int] -> Substitution' Term
forall {a}.
(SubstArg a ~ a, Subst a, DeBruijn a) =>
[Int] -> Substitution' a
weak ([Int] -> Substitution' Term) -> [Int] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. Ord a => [a] -> [a]
List.sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Bool) -> Int
forall a b. (a, b) -> a
fst [(Int, Bool)]
alpha) Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
b)
            ([(Term, Bool)], Term) -> TCMT IO ([(Term, Bool)], Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Int, Bool) -> (Term, Bool)) -> [(Int, Bool)] -> [(Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Int -> Term) -> (Int, Bool) -> (Term, Bool)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Int -> Term
var) [(Int, Bool)]
alpha,Term
u)

      reportSDoc "tc.sys.cover.sys" 20 $ fsep $ prettyTCM gamma : map' prettyTCM sys
      reportSDoc "tc.sys.cover.sys" 40 $ fsep $ (text . show) gamma : map' (text . show) sys
      return (System gamma 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
_ [Int]
_ Type'' Term Term
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 -> IsWithFunction Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClauseLHS :: forall a.
Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type'' Term Term
t IsWithFunction (Substitution' Term)
withSub c :: SpineClause
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
_rhs0 WhereDeclarations
_wh Catchall
_catchall) LHSResult -> TCM a
ret = do
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking clause" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ SpineClause -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA SpineClause
c
    () <- [NamedArg (Pattern' Expr)]
-> (List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
trailingWithPatterns [NamedArg (Pattern' Expr)]
aps) ((List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ())
-> (List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ List1 (NamedArg (Pattern' Expr))
withPats -> do
      TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (Pattern' Expr) -> TypeError
UnexpectedWithPatterns (NonEmpty (Pattern' Expr) -> TypeError)
-> NonEmpty (Pattern' Expr) -> TypeError
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> Pattern' Expr)
-> List1 (NamedArg (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg List1 (NamedArg (Pattern' Expr))
withPats
    traceCall (CheckClause t c) $ do
      aps <- expandPatternSynonyms aps
      unless (null strippedPats) $ reportSDoc "tc.lhs.top" 50 $
        "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
      closed_t <- flip abstract t <$> getContextTelescope
      checkLeftHandSide (CheckLHS lhs) (getRange lhs) (ClauseLHS x) aps t withSub strippedPats ret

-- | Type check a function clause.

checkClause
  :: Type
       -- ^ Type of function defined by this clause.
  -> IsWithFunction (QName, Substitution, Map Name LetBinding)
       -- ^ Parent function, module parameter substitution arising from with-abstraction, and inherited let-bindings.
  -> A.SpineClause
       -- ^ Clause.
  -> TCM (Clause, ClausesPostChecks)
       -- ^ Type-checked clause

checkClause :: Type'' Term Term
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type'' Term Term
t IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
withSubAndLets c :: SpineClause
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
rhs0 WhereDeclarations
wh Catchall
catchall) = do
  let withSub :: IsWithFunction (Substitution' Term)
withSub = (QName, Substitution' Term, Map Name LetBinding)
-> Substitution' Term
forall a b c. (a, b, c) -> b
snd3 ((QName, Substitution' Term, Map Name LetBinding)
 -> Substitution' Term)
-> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
-> IsWithFunction (Substitution' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
withSubAndLets
  cxtNames <- TCMT IO [Name]
forall (m :: * -> *). MonadTCEnv m => m [Name]
getContextNames
  checkClauseLHS t withSub c $ \ lhsResult :: LHSResult
lhsResult@(LHSResult Int
npars Tele (Dom (Type'' Term Term))
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg (Type'' Term Term)
trhs Substitution' Term
patSubst [AsBinding]
asb IntSet
psplit Bool
ixsplit) -> do

    let installInheritedLets :: TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
installInheritedLets TCMT IO (Clause, ClausesPostChecks)
k
          | WithFunction (QName
_f, Substitution' Term
withSub, Map Name LetBinding
lets) <- IsWithFunction (QName, Substitution' Term, Map Name LetBinding)
withSubAndLets = do
            lets' <- (LetBinding -> TCMT IO (Open LetBinding))
-> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse LetBinding -> TCMT IO (Open LetBinding)
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen (Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding)))
-> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Map Name LetBinding))
-> Map Name LetBinding -> Map Name LetBinding
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' Term
patSubst Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
withSub) Map Name LetBinding
lets
            locallyTC eLetBindings (lets' <>) k
          | Bool
otherwise = TCMT IO (Clause, ClausesPostChecks)
k

    TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
installInheritedLets (TCMT IO (Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ 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.
        t' <- case IsWithFunction (Substitution' Term)
withSub of
                WithFunction{} -> Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
t
                IsWithFunction (Substitution' Term)
NoWithFunction -> do
                  theta <- ModuleName -> TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Tele (Dom (Type'' Term Term)))
lookupSection (QName -> ModuleName
qnameModule QName
x)
                  return $! abstract theta 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
updateRHS RHS
rhs0
            updateRHS rhs :: RHS
rhs@A.RHS{}               = RHS
rhs
            updateRHS rhs :: RHS
rhs@A.AbsurdRHS{}         = RHS
rhs
            updateRHS (A.WithRHS QName
q List1 WithExpr
es List1 Clause
cs)       = QName -> List1 WithExpr -> List1 Clause -> RHS
A.WithRHS QName
q List1 WithExpr
es (List1 Clause -> RHS) -> List1 Clause -> RHS
forall a b. (a -> b) -> a -> b
$ (Clause -> Clause) -> List1 Clause -> List1 Clause
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Clause
updateClause List1 Clause
cs
            updateRHS (A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) =
              [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [ProblemEq])
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh

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

        (body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult 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).

        wbody <- unsafeInTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with

        body <- return $! body `mplus` wbody

        whenM (optDoubleCheck <$> pragmaOptions) $ case body of
          Just Term
v  -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"double checking rhs"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM (Arg (Type'' Term Term) -> Type'' Term Term
forall e. Arg e -> e
unArg Arg (Type'' Term Term)
trhs))
              ]
            TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning 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.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Comparison -> TypeOf Term -> TCM ()
forall a. CheckInternal a => a -> Comparison -> TypeOf a -> TCM ()
checkInternal Term
v Comparison
CmpLeq (TypeOf Term -> TCM ()) -> TypeOf Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Arg (TypeOf Term) -> TypeOf Term
forall e. Arg e -> e
unArg Arg (TypeOf Term)
Arg (Type'' Term Term)
trhs
          Maybe Term
Nothing -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        reportSDoc "tc.lhs.top" 10 $ vcat
          [ "Clause before translation:"
          , nest 2 $ vcat
            [ "delta =" <+> prettyTCM delta
            , "ps    =" <+> do P.fsep <$> prettyTCMPatterns ps
            , "body  =" <+> maybe "_|_" prettyTCM body
            , "type  =" <+> prettyTCM t
            ]
          ]

        reportSDoc "tc.lhs.top" 90 $ vcat
          [ "Clause before translation (raw):"
          , nest 2 $ vcat
            [ "ps    =" <+> text (show ps)
            , "body  =" <+> text (show body)
            , "type  =" <+> text (show t)
            ]
          ]

        -- compute body modification for irrelevant definitions, see issue 610
        rel <- viewTC eRelevance
        let bodyMod = Bool -> (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel) ((Term -> Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare)

        -- absurd clauses don't define computational behaviour, so it's fine to
        -- treat them as catchalls.
        let catchall' = if Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
body then Range' SrcFile -> Catchall
YesCatchall Range' SrcFile
forall a. Null a => a
empty else Catchall
catchall

        return $! (, CPC psplit)
          Clause { clauseLHSRange  = getRange i
                 , clauseFullRange = getRange c
                 , clauseTel       = killRange delta
                 , namedClausePats = ps
                 , clauseBody      = bodyMod body
                 , clauseType      = Just trhs
                 , clauseCatchall  = catchall'
                 , clauseRecursive   = MaybeRecursive -- we don't know yet
                 , clauseUnreachable = Nothing -- we don't know yet
                 , clauseEllipsis    = lhsEllipsis i
                 , clauseWhereModule = A.whereModule wh
                 }



-- | Generate the abstract pattern corresponding to Refl
getReflPattern :: TCM A.Pattern
getReflPattern :: TCM (Pattern' Expr)
getReflPattern = do
  -- Get the name of builtin REFL.
  Con reflCon _ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl

  reflInfo <- fmap (setOrigin Inserted) <$> getReflArgInfo reflCon
  let patInfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager
  -- The REFL constructor might have an argument
  let reflArg = Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
forall a. Maybe a -> [a]
maybeToList (Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)])
-> Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> NamedArg (Pattern' Expr))
-> Maybe ArgInfo -> Maybe (NamedArg (Pattern' Expr))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ ArgInfo
ai -> ArgInfo
-> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Named NamedName (Pattern' Expr)
forall a name. a -> Named name a
unnamed (Pattern' Expr -> Named NamedName (Pattern' Expr))
-> Pattern' Expr -> Named NamedName (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) Maybe ArgInfo
reflInfo

  pure $ A.ConP patInfo (unambiguous $ conName reflCon) reflArg

-- | 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'' Term Term
-> LHSResult
-> RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps Type'' Term Term
t lhsResult :: LHSResult
lhsResult@(LHSResult Int
_ Tele (Dom (Type'' Term Term))
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg (Type'' Term Term)
trhs Substitution' Term
_ [AsBinding]
_asb IntSet
_ Bool
_) 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 List1 WithExpr
es List1 Clause
cs        -> QName
-> List1 WithExpr
-> List1 Clause
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux List1 WithExpr
es List1 Clause
cs

  -- Ordinary case: f xs = e
  ordinaryRHS :: A.Expr -> TCM (Maybe Term, WithFunctionProblem)
  ordinaryRHS :: Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS Expr
e = Account (BenchPhase (TCMT IO))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.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@.
    mv <- if Bool
absurdPat
          then Maybe Term
forall a. Maybe a
Nothing Maybe Term -> TCM () -> TCMT IO (Maybe Term)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do Expr -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
e (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
AbsurdPatternRequiresAbsentRHS
          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'' Term Term -> TCMT IO Term
checkExpr Expr
e (Arg (Type'' Term Term) -> Type'' Term Term
forall e. Arg e -> e
unArg Arg (Type'' Term Term)
trhs)
    return (mv, NoWithFunction)

  -- Absurd case: no right hand side
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS = do
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless Bool
absurdPat (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
AbsentRHSRequiresAbsurdPattern
    (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing, WithFunctionProblem
forall a. IsWithFunction a
NoWithFunction)

  -- With case: @f xs with {a} in eqa | b in eqb | {{c}} | ...; ... | ps1 = rhs1; ... | ps2 = rhs2; ...@
  -- We need to modify the patterns `ps1, ps2, ...` in the user-provided clauses
  -- to insert the {eqb} names so that the equality proofs are available on the various RHS.
  withRHS ::
       QName             -- name of the with-function
    -> List1 A.WithExpr  -- @[{a} in eqa, b in eqb, {{c}}, ...]@
    -> List1 A.Clause    -- @[(ps1 = rhs1), (ps2 = rhs), ...]@
    -> TCM (Maybe Term, WithFunctionProblem)
  withRHS :: QName
-> List1 WithExpr
-> List1 Clause
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux List1 WithExpr
es List1 Clause
cs = do

    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"TC.Rules.Def.checkclause reached A.WithRHS"
      , NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA QName
aux TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<| (WithExpr -> TCMT IO Doc)
-> List1 WithExpr -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc)
-> (WithExpr -> TCMT IO Doc) -> WithExpr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> TCMT IO Doc)
-> (WithExpr -> Arg Expr) -> WithExpr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithExpr -> Arg Expr
forall name a. Named name a -> a
namedThing) List1 WithExpr
es
      ]
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      nfv <- TCM Int
getCurrentModuleFreeVars
      m   <- currentModule
      sep [ "with function module:" <+>
             prettyList (map' prettyTCM $ mnameToList m)
          ,  text $ "free variables: " ++! show nfv
          ]

    -- Infer the types of the with expressions

    vtys <- List1 WithExpr
-> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 WithExpr
es ((WithExpr -> TCMT IO (Arg (Term, EqualityView)))
 -> TCMT IO (NonEmpty (Arg (Term, EqualityView))))
-> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Arg Expr
we) -> do
              (e, ty) <- Arg Expr -> TCM (Term, Type'' Term Term)
inferExprForWith Arg Expr
we
              pure $ (<$ we) . (e,) $ case nm of
                Maybe BindName
Nothing -> Type'' Term Term -> EqualityView
OtherType Type'' Term Term
ty
                Just{}  -> Type'' Term Term -> EqualityView
IdiomType Type'' Term Term
ty

    let names = (WithExpr -> Arg (Maybe BindName))
-> List1 WithExpr -> List1 (Arg (Maybe BindName))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Named Maybe BindName
nm Arg Expr
e) -> Maybe BindName
nm Maybe BindName -> Arg Expr -> Arg (Maybe BindName)
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Expr
e) List1 WithExpr
es
    cs <- pure $ for cs $ mapLHSCores (insertInspects names)

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

    checkWithRHS x aux t lhsResult vtys 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 ([RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem))
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$
        [(QName, Expr)]
-> [RewriteEqn]
-> (NonEmpty (QName, Expr) -> [RewriteEqn])
-> [RewriteEqn]
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [(QName, Expr)]
qes {-then-} [RewriteEqn]
rs {-else-} ((NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn])
-> (NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn]
forall a b. (a -> b) -> a -> b
$ \ NonEmpty (QName, Expr)
qes -> NonEmpty (QName, Expr) -> RewriteEqn
forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite NonEmpty (QName, Expr)
qes RewriteEqn -> [RewriteEqn] -> [RewriteEqn]
forall a. a -> [a] -> [a]
: [RewriteEqn]
rs
    Invert QName
qname List1 (Named BindName (Pattern' Expr, Expr))
pes -> QName
-> List1 (Named BindName (Pattern' Expr, Expr))
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname List1 (Named BindName (Pattern' Expr, Expr))
pes [RewriteEqn]
rs
    LeftLet NonEmpty (Pattern' Expr, Expr)
pes -> NonEmpty (Pattern' Expr, Expr)
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS NonEmpty (Pattern' Expr, Expr)
pes [RewriteEqn]
rs

    where

    -- @using@ clauses
    usingEqnRHS :: List1 (A.Pattern, A.Expr) -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    usingEqnRHS :: NonEmpty (Pattern' Expr, Expr)
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS NonEmpty (Pattern' Expr, Expr)
pes [RewriteEqn]
rs = do
      let letBindings :: [LetBinding]
letBindings = [(Pattern' Expr, Expr)]
-> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (NonEmpty (Pattern' Expr, Expr)
-> [Item (NonEmpty (Pattern' Expr, Expr))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (Pattern' Expr, Expr)
pes) (((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding])
-> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
forall a b. (a -> b) -> a -> b
$ \(Pattern' Expr
p, Expr
e) -> LetInfo -> ArgInfo -> Pattern' Expr -> Expr -> LetBinding
A.LetPatBind (Range' SrcFile -> LetInfo
LetRange (Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Expr
e)) ArgInfo
defaultArgInfo Pattern' Expr
p Expr
e
      [LetBinding]
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings' [LetBinding]
letBindings (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [RewriteEqn]
rs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh

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

      let (List1 (Named BindName (Pattern' Expr))
npats, List1 (Named BindName Expr)
es) = (Named BindName (Pattern' Expr, Expr)
 -> (Named BindName (Pattern' Expr), Named BindName Expr))
-> List1 (Named BindName (Pattern' Expr, Expr))
-> (List1 (Named BindName (Pattern' Expr)),
    List1 (Named BindName Expr))
forall a b c. (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
List1.unzipWith (\ (Named Maybe BindName
nm (Pattern' Expr
p , Expr
e)) -> (Maybe BindName -> Pattern' Expr -> Named BindName (Pattern' Expr)
forall name a. Maybe name -> a -> Named name a
Named Maybe BindName
nm Pattern' Expr
p, Maybe BindName -> Expr -> Named BindName Expr
forall name a. Maybe name -> a -> Named name a
Named Maybe BindName
nm Expr
e)) List1 (Named BindName (Pattern' Expr, Expr))
pes
      -- Infer the types of the with expressions
      vtys <- List1 (Named BindName Expr)
-> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 (Named BindName Expr)
es ((Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
 -> TCMT IO (NonEmpty (Arg (Term, EqualityView))))
-> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Expr
we) -> do
        (e, ty) <- Arg Expr -> TCM (Term, Type'' Term Term)
inferExprForWith (Expr -> Arg Expr
forall a. a -> Arg a
defaultArg Expr
we)
        pure $ defaultArg . (e,) $ case nm of
          Maybe BindName
Nothing -> Type'' Term Term -> EqualityView
OtherType Type'' Term Term
ty
          Just{}  -> Type'' Term Term -> EqualityView
IdiomType Type'' Term Term
ty

      let pats = (Pattern' Expr -> Arg (Pattern' Expr))
-> NonEmpty (Pattern' Expr) -> NonEmpty (Arg (Pattern' Expr))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg (NonEmpty (Pattern' Expr) -> NonEmpty (Arg (Pattern' Expr)))
-> NonEmpty (Pattern' Expr) -> NonEmpty (Arg (Pattern' Expr))
forall a b. (a -> b) -> a -> b
$ NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr))
-> NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$
            List1 (Named BindName (Pattern' Expr))
-> (Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
-> NonEmpty (NonEmpty (Pattern' Expr))
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for List1 (Named BindName (Pattern' Expr))
npats ((Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
 -> NonEmpty (NonEmpty (Pattern' Expr)))
-> (Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
-> NonEmpty (NonEmpty (Pattern' Expr))
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Pattern' Expr
p) -> Pattern' Expr
p Pattern' Expr -> [Pattern' Expr] -> NonEmpty (Pattern' Expr)
forall a. a -> [a] -> NonEmpty a
:| [Pattern' Expr]
-> (BindName -> [Pattern' Expr])
-> Maybe BindName
-> [Pattern' Expr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ BindName
n -> [BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP BindName
n]) Maybe BindName
nm

      -- 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.
      solveSizeConstraints DefaultToInfty

      let rhs' = NonEmpty (Arg (Pattern' Expr)) -> RHS -> RHS
insertPatterns NonEmpty (Arg (Pattern' Expr))
pats RHS
rhs
          (rhs'', outerWhere) -- the where clauses should go on the inner-most with
            | null rs  = (rhs', wh)
            | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
          -- Andreas, 2014-03-05 kill range of copied patterns
          -- since they really do not have a source location.
          cl = LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> 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
$ NonEmpty (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore NonEmpty (Arg (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 Catchall
forall a. Null a => a
empty

      reportSDoc "tc.invert" 60 $ vcat
        [ text "invert"
        , "  rhs' = " <> (text . show) rhs'
        ]
      checkWithRHS x qname t lhsResult vtys $ singleton 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.
      st <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      -- TODO:: recurse defined but not used
      let recurse = do
           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 = 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
-> Getting InteractionPoints TCState InteractionPoints
-> InteractionPoints
forall s a. s -> Getting a s a -> a
^. Getting InteractionPoints TCState InteractionPoints
Lens' TCState InteractionPoints
stInteractionPoints)
           when (sameIP st st') $ putTC st
           handleRHS $ A.RewriteRHS rs strippedPats rhs wh

      -- Get value and type of rewrite-expression.

      (proof, eqt) <- inferExpr eq

      -- Andreas, 2024-02-27, issue #7150
      -- trigger instance search to resolve instances in rewrite-expression
      solveAwakeConstraints

      -- 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.
      solveSizeConstraints DefaultToInfty

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

      t' <- reduce =<< instantiateFull eqt
      (eqt, rewriteType, rewriteFrom, rewriteTo) <- equalityView (getRange eq) t' >>= \case
        eqt :: EqualityView
eqt@(EqualityType Range' SrcFile
_r Sort
_s QName
_eq [Arg Term]
_params (Arg ArgInfo
_ Term
dom) Arg Term
a Arg Term
b) -> do
          s <- Term -> TCMT IO Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
dom
          return (eqt, El s dom, unArg a, unArg 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, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type'' Term Term, Term, Term))
-> TypeError
-> TCMT IO (EqualityView, Type'' Term Term, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
CannotRewriteByNonEquation Type'' Term Term
t'
        IdiomType{} -> TypeError -> TCMT IO (EqualityView, Type'' Term Term, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type'' Term Term, Term, Term))
-> TypeError
-> TCMT IO (EqualityView, Type'' Term Term, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
CannotRewriteByNonEquation Type'' Term Term
t'

      reflPat <- getReflPattern

      -- 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 = TCM () -> TCMT IO Bool
tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
           Type'' Term Term -> Term -> Term -> TCM ()
equalTerm Type'' Term Term
rewriteType Term
rewriteFrom Term
rewriteTo

      (pats', withExpr, withType) <- do
        ifM isReflexive
          {-then-} (return (                      reflPat :| [], proof, OtherType t'))
          {-else-} (return (A.WildP patNoRange <| reflPat :| [], proof, eqt))
      let pats = Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
-> NonEmpty (Pattern' Expr) -> NonEmpty (Arg (Pattern' Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Pattern' Expr)
pats'

      let rhs' = NonEmpty (Arg (Pattern' Expr)) -> RHS -> RHS
insertPatterns NonEmpty (Arg (Pattern' Expr))
pats RHS
rhs
          (rhs'', outerWhere) -- the where clauses should go on the inner-most with
            | null rs  = (rhs', wh)
            | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
          -- Andreas, 2014-03-05 kill range of copied patterns
          -- since they really do not have a source location.
          cl = LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> 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
$ NonEmpty (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore NonEmpty (Arg (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 Catchall
forall a. Null a => a
empty

      reportSDoc "tc.rewrite" 60 $ vcat
        [ text "rewrite"
        , "  rhs' = " <> (text . show) rhs'
        ]
      checkWithRHS x qname t lhsResult (singleton $ defaultArg (withExpr, withType)) $ singleton cl

checkWithRHS
  :: QName                             -- ^ Name of function.
  -> QName                             -- ^ Name of the with-function.
  -> Type                              -- ^ Type of function.
  -> LHSResult                         -- ^ Result of type-checking patterns
  -> List1 (Arg (Term, EqualityView))  -- ^ Expressions and types of with-expressions.
  -> List1 A.Clause                    -- ^ With-clauses to check.
  -> TCM (Maybe Term, WithFunctionProblem)
                                -- Note: as-bindings already bound (in checkClause)
checkWithRHS :: QName
-> QName
-> Type'' Term Term
-> LHSResult
-> NonEmpty (Arg (Term, EqualityView))
-> List1 Clause
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type'' Term Term
t (LHSResult Int
npars Tele (Dom (Type'' Term Term))
delta [NamedArg DeBruijnPattern]
ps Bool
_absurdPat Arg (Type'' Term Term)
trhs Substitution' Term
_ [AsBinding]
_asb IntSet
_ Bool
_) NonEmpty (Arg (Term, EqualityView))
vtys0 List1 Clause
cs =
  [Char]
-> Int
-> [Char]
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.with.top" Int
25 [Char]
"checkWithRHS" (TCM (Maybe Term, WithFunctionProblem)
 -> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
    Account (BenchPhase (TCMT IO))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.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
        withArgs <- NonEmpty (Arg (Term, EqualityView)) -> TCM (NonEmpty (Arg Term))
withArguments NonEmpty (Arg (Term, EqualityView))
vtys0
        let 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
$ [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm [NamedArg DeBruijnPattern]
ps

        reportSDoc "tc.with.top" 30 $ vcat $
          -- declared locally because we do not want to use the unzip'd thing!
          let (vs, as) = List1.unzipWith unArg vtys0 in
          [ "vs (before normalization) =" <+> prettyTCM vs
          , "as (before normalization) =" <+> prettyTCM as
          ]
        reportSDoc "tc.with.top" 45 $ vcat $
          -- declared locally because we do not want to use the unzip'd thing!
          let (vs, as) = List1.unzipWith unArg vtys0 in
          [ "vs (before norm., raw) =" <+> pretty vs
          ]
        vtys0 <- normalise vtys0

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
          [ "delta  =" <+> prettyTCM delta
          ]
        reportSDoc "tc.with.top" 25 $ vcat $
          -- declared locally because we do not want to use the unzip'd thing!
          let (vs, as) = List1.unzipWith unArg vtys0 in
          [ "vs     =" <+> prettyTCM vs
          , "as     =" <+> prettyTCM as
          , "perm   =" <+> text (show perm)
          ]

        -- Split the telescope into the part needed to type the with arguments
        -- and all the other stuff
        let (delta1, delta2, perm', t', vtys) = splitTelForWith delta (unArg trhs) vtys0
        let finalPerm = Permutation -> Permutation -> Permutation
composeP Permutation
perm' Permutation
perm

        reportSLn "tc.with.top" 75 $ "delta  = " ++! show delta

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
          [ "delta1 =" <+> prettyTCM delta1
          , "delta2 =" <+> addContext delta1 (prettyTCM delta2)
          ]
        reportSDoc "tc.with.top" 25 $ vcat
          [ "perm'  =" <+> text (show perm')
          , "fPerm  =" <+> text (show finalPerm)
          ]

        -- Create the body of the original function

        -- All the context variables
        us <- getContextTerms
        let n = [Term] -> Int
forall a. Sized a => a -> Int
size [Term]
us
            m = Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
delta
            -- First the variables bound outside this definition
            (us0, us1') = splitAt' (n - m) us
            -- Then permute the rest and grab those needed to for the with arguments
            (us1, us2)  = splitAt' (size delta1) $ permute perm' us1'
            -- Now stuff the with arguments in between and finish with the remaining variables
            argsS = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Term]
us0 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
us1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg (NonEmpty (Arg Term) -> [Item (NonEmpty (Arg Term))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (Arg Term)
withArgs) [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
us2
            v         = Maybe a
forall a. Maybe a
Nothing -- generated by checkWithFunction
        -- Andreas, 2013-02-26 add with-name to signature for printing purposes
        addConstant aux =<< do
          lang <- getLanguage
          useTerPragma =<<
            defaultDefn defaultArgInfo aux __DUMMY_TYPE__ lang <$>
              emptyFunction

        reportSDoc "tc.with.top" 20 $ vcat $
          let (vs, as) = List1.unzipWith unArg vtys in
          -- Andreas, 2025-04-07, escapeContext impossible Δ leads to crash if e.g. vs has metas defined in Δ.
          -- Thus, we use unsafeEscapeContext instead.
          [ "    with arguments" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (fmap prettyTCM vs)
          , "             types" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (fmap prettyTCM as)
          , "           context" <+> (prettyTCM =<< getContextTelescope)
          , "             delta" <+> do escapeContext impossible (size delta) $ prettyTCM delta
          , "            delta1" <+> do escapeContext impossible (size delta) $ prettyTCM delta1
          , "            delta2" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyTCM delta2
          ]

        -- Only inherit user-written let bindings from parent clauses. Others, like @-patterns,
        -- should not be carried over.
        lets <- Map.filter ((== UserWritten) . letOrigin) <$> (traverse getOpen =<< viewTC eLetBindings)

        return (v, WithFunction (WithFunctionProblemData x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs argsS lets))

-- | Invoked in empty context.
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCMT IO (Maybe Term)
checkWithFunction [Name]
_ WithFunctionProblem
NoWithFunction = Maybe Term -> TCMT IO (Maybe Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
checkWithFunction [Name]
cxtNames (WithFunction (WithFunctionProblemData QName
f QName
aux Type'' Term Term
t Tele (Dom (Type'' Term Term))
delta Tele (Dom (Type'' Term Term))
delta1 Tele (Dom (Type'' Term Term))
delta2 NonEmpty (Arg (Term, EqualityView))
vtys Type'' Term Term
b [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm' Permutation
perm Permutation
finalPerm List1 Clause
cs Substitution' Term
argsS Map Name LetBinding
lets)) = do
  let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
      withSub :: Substitution
      withSub :: Substitution' Term
withSub = let as :: NonEmpty EqualityView
as = (Arg (Term, EqualityView) -> EqualityView)
-> NonEmpty (Arg (Term, EqualityView)) -> NonEmpty EqualityView
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (Arg (Term, EqualityView) -> (Term, EqualityView))
-> Arg (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg) NonEmpty (Arg (Term, EqualityView))
vtys in
                Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
delta2) (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS (NonEmpty EqualityView -> Int
forall (f :: * -> *).
(Functor f, Foldable f) =>
f EqualityView -> Int
countWithArgs NonEmpty EqualityView
as) Substitution' Term
forall a. Substitution' a
idS)
                Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Impossible -> Permutation -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm')

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkWithFunction"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      let (NonEmpty Term
vs, NonEmpty EqualityView
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> NonEmpty (Arg (Term, EqualityView))
-> (NonEmpty Term, NonEmpty EqualityView)
forall a b c. (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
List1.unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg NonEmpty (Arg (Term, EqualityView))
vtys in
      [ TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom (Type'' Term Term)) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Tele (Dom (Type'' Term Term)) -> m Doc
prettyTCM Tele (Dom (Type'' Term Term))
delta1
      , TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta1 (Tele (Dom (Type'' Term Term)) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Tele (Dom (Type'' Term Term)) -> m Doc
prettyTCM Tele (Dom (Type'' Term Term))
delta2)
      , TCMT IO Doc
"t      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
      , TCMT IO Doc
"as     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta1 (NonEmpty EqualityView -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
NonEmpty EqualityView -> m Doc
prettyTCM NonEmpty EqualityView
as)
      , TCMT IO Doc
"vs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NonEmpty Term -> m Doc
prettyTCM NonEmpty Term
vs
      , TCMT IO Doc
"b      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
b
      , TCMT IO Doc
"qs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom (Type'' Term Term)) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom (Type'' Term Term))
delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> TCMT IO Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
qs
      , TCMT IO Doc
"perm'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm')
      , TCMT IO Doc
"perm   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
      , TCMT IO Doc
"fperm  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
finalPerm)
      , TCMT IO Doc
"withSub=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Substitution' Term -> [Char]
forall a. Show a => a -> [Char]
show Substitution' Term
withSub)
      ]
    ]

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

  -- Jesper, 2020-04-05: Currently variable generalization inserts
  -- dummy terms, we have to reduce projections to get rid of them.
  -- (see also #1332).
  let reds :: SmallSet AllowedReduction
reds = [AllowedReduction] -> SmallSet AllowedReduction
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions]
  delta1 <- (SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> TCMT IO (Tele (Dom (Type'' Term Term)))
-> TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *) a.
MonadTCEnv m =>
(SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> m a -> m a
modifyAllowedReductions (SmallSet AllowedReduction
-> SmallSet AllowedReduction -> SmallSet AllowedReduction
forall a b. a -> b -> a
const SmallSet AllowedReduction
reds) (TCMT IO (Tele (Dom (Type'' Term Term)))
 -> TCMT IO (Tele (Dom (Type'' Term Term))))
-> TCMT IO (Tele (Dom (Type'' Term Term)))
-> TCMT IO (Tele (Dom (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term))
-> TCMT IO (Tele (Dom (Type'' Term Term)))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom (Type'' Term Term))
delta1

  -- Amy, 2025-05-14: (InstanceHack) we have to flush instances that may
  -- come from previous clauses, see #7882.
  flushInstanceConstraints

  -- Generate the type of the with function
  (withFunType, (nwithargs, nwithpats)) <- do
    let ps = Impossible -> Permutation -> Substitution' DeBruijnPattern
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm') Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [NamedArg DeBruijnPattern]
qs
    reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
                                  $ text "ps =" <+> pretty ps
    let vs = [NamedArg DeBruijnPattern] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg DeBruijnPattern]
ps
    bndry <- if null vs then return empty else do
      iz <- primIZero
      io <- primIOne
      let tm = QName -> Elims -> Term
Def QName
f ([NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ps)
      return $! Boundary [(i,(inplaceS i iz `applySubst` tm, inplaceS i io `applySubst` tm)) | i <- vs]
    reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
                                  $ text "bndry =" <+> pretty bndry
    withFunctionType delta1 vtys delta2 b bndry
  reportSDoc "tc.with.type" 10 $ sep [ "with-function type:", nest 2 $ prettyTCM withFunType ]
  reportSDoc "tc.with.type" 50 $ sep [ "with-function type:", nest 2 $ pretty withFunType ]

  call_in_parent <- do
    (TelV tel _,bs) <- telViewUpToPathBoundary' (nwithargs + size delta) withFunType
    return $ argsS `applySubst` Def aux (teleElims tel bs)

  reportSDoc "tc.with.top" 20 $ addContext delta $ "with function call" <+> prettyTCM call_in_parent

  -- Andreas, 2013-10-21
  -- Check generated type directly in internal syntax.
  setCurrentRange cs $
    traceCall NoHighlighting $   -- To avoid flicker.
    traceCall (CheckWithFunctionType withFunType) $
    -- Jesper, 2024-07-10, issue #6841:
    -- Having an ill-typed type can lead to problems in the
    -- coverage checker, so we ensure there are no constraints here.
    noConstraints $ checkType withFunType

  reportSLn "tc.with.top" 20 "creating with display form..."

  -- With display forms are closed
  df <- inTopContext $ makeOpen =<< withDisplayForm f aux delta1 delta2 nwithargs qs perm' perm

  reportSLn "tc.with.top" 20 "created with display form"

  case dget df of
    Display Int
n Elims
ts DisplayTerm
dt ->
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Display" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
        , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elims
ts
        , DisplayTerm -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM DisplayTerm
dt
        ]
  addConstant aux =<< do
    lang <- getLanguage
    fun  <- emptyFunction
    useTerPragma $
      (defaultDefn defaultArgInfo aux withFunType lang fun)
        { defDisplay = [df] }
  -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

  reportSDoc "tc.with.top" 10 $ sep
    [ "added with function" <+> (prettyTCM aux) <+> "of type"
    , nest 2 $ prettyTCM withFunType
    , nest 2 $ "-|" <+> (prettyTCM =<< getContextTelescope)
    ]
  reportSDoc "tc.with.top" 70 $ vcat
    [ nest 2 $ text $ "raw with func. type = " ++! show withFunType
    ]


  -- Construct the body for the with function
  cs <- return $! fmap (A.lhsToSpine) cs
  cs <- buildWithFunction cxtNames f aux t delta qs npars withSub finalPerm (size delta1) nwithpats cs
  cs <- return $! fmap (A.spineToLhs) cs

  -- #4833: inherit abstract mode from parent
  abstr <- defAbstract <$> ignoreAbstractMode (getConstInfo f)

  -- Check the with function
  let info = Name
-> Fixity'
-> Access
-> IsAbstract
-> Range' SrcFile
-> DefInfo' Expr
forall t.
Name
-> Fixity' -> Access -> IsAbstract -> Range' SrcFile -> 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
abstr (List1 Clause -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange List1 Clause
cs)
  ai <- defArgInfo <$> getConstInfo f
  checkFunDefS withFunType ai Nothing (WithFunction (f, withSub, lets)) info aux $ List1.toList cs
  return $ Just $ call_in_parent

-- | Type check a where clause.
checkWhere
  :: A.WhereDeclarations -- ^ Where-declarations to check.
  -> TCM a               -- ^ Continuation.
  -> TCM a
checkWhere :: forall a. WhereDeclarations -> TCM a -> TCM a
checkWhere wh :: WhereDeclarations
wh@(A.WhereDecls Maybe ModuleName
whmod Bool
whNamed Maybe Declaration
mds) TCM a
ret = do
  Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Bool -> Bool
not Bool
whNamed) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Maybe ModuleName -> TCM ()
forall {m :: * -> *}.
(MonadTrace m, HasOptions m, MonadDebug m, MonadError TCErr m) =>
Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
whmod
  case Maybe Declaration
mds of
      Maybe Declaration
Nothing -> TCM a
ret
      Just (A.Section Range' SrcFile
_ Erased
e ModuleName
m GeneralizeTelescope
tel [Declaration]
ds) -> do

        -- Andreas, 2025-06-14, issue #7943.
        -- If we are in erased context, mark the module as erased.
        e <- case Erased
e of
          NotErased QωOrigin
oo -> do
            Lens' TCEnv Quantity -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity TCMT IO Quantity -> (Quantity -> TCMT IO Erased) -> TCMT IO Erased
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Quantity0 Q0Origin
o -> do
                Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (QωOrigin
oo QωOrigin -> QωOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== QωOrigin
QωInferred) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
                  QωOrigin -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QωOrigin
oo (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QωOrigin -> Warning
PlentyInHardCompileTimeMode QωOrigin
oo
                Erased -> TCMT IO Erased
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Erased -> TCMT IO Erased) -> Erased -> TCMT IO Erased
forall a b. (a -> b) -> a -> b
$ Q0Origin -> Erased
Erased Q0Origin
o
              Quantityω{} -> Erased -> TCMT IO Erased
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Erased
e
              Quantity1{} -> TCMT IO Erased
forall a. HasCallStack => a
__IMPOSSIBLE__
          Erased{}      -> Erased -> TCMT IO Erased
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Erased
e

        localTC whereEnv $ newSection e m tel $ checkDecls ds
        -- Andreas, 2025-06-14, issue #7944
        -- We need to check the body in its original erasure status.
        withCurrentModule m ret
      Maybe Declaration
_ -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    whereEnv :: TCEnv -> TCEnv
whereEnv = ASetter TCEnv TCEnv WhereClause_ WhereClause_
-> WhereClause_ -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set' ASetter TCEnv TCEnv WhereClause_ WhereClause_
Lens' TCEnv WhereClause_
eCheckingWhere (if Bool
whNamed then WhereClause_
C.SomeWhere_ else WhereClause_
C.AnyWhere_)

    -- #2897: We can't handle named where-modules in refined contexts.
    ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    ensureNoNamedWhereInRefinedContext (Just ModuleName
m) = Call -> m () -> m ()
forall a. Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (ModuleName -> Call
CheckNamedWhere ModuleName
m) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      args <- (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> m [Arg Term] -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> m [Arg Term]
forall (m :: * -> *).
(HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> m [Arg Term]) -> m ModuleName -> m [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
      unless (isWeakening args) $ do -- weakened contexts are fine
        names <- map' (argNameToString . fst . unDom) . telToList <$>
                (lookupSection =<< currentModule)
        typeError $ NamedWhereModuleInRefinedContext args names
      where
        isWeakening :: [Term] -> Bool
isWeakening [] = Bool
True
        isWeakening (Var Int
i [] : [Term]
args) = Int -> [Term] -> Bool
isWk (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Term]
args
          where
            isWk :: Int -> [Term] -> Bool
isWk Int
i []                = Bool
True
            isWk Int
i (Var Int
j [] : [Term]
args) = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Int -> [Term] -> Bool
isWk (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Term]
args
            isWk Int
_ [Term]
_ = Bool
False
        isWeakening [Term]
_ = Bool
False


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

newSection ::
  Erased -> ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
newSection :: forall a.
Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection Erased
e ModuleName
m gtel :: GeneralizeTelescope
gtel@(A.GeneralizeTel Map QName Name
_ Telescope
tel) TCM a
cont = do
  -- If the section is erased, then hard compile-time mode is entered.
  Erased -> TCM ()
warnForPlentyInHardCompileTimeMode Erased
e
  Erased -> TCM a -> TCM a
forall a. Erased -> TCM a -> TCM a
setHardCompileTimeModeIfErased Erased
e (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"checking section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Erased -> Doc -> Doc
prettyErased Erased
e (Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((TypedBinding -> TCMT IO Doc) -> Telescope -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' TypedBinding -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Telescope
tel)

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

    ModuleName -> TCM ()
addSection ModuleName
m

    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"actual tele:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom (Type'' Term Term)) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Tele (Dom (Type'' Term Term)) -> m Doc
prettyTCM (Tele (Dom (Type'' Term Term)) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom (Type'' Term Term))) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Tele (Dom (Type'' Term Term)))
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 -> IsWithFunction Substitution -> A.SpineClause -> TCM a -> TCM a
atClause :: forall a.
QName
-> Int
-> Type'' Term Term
-> IsWithFunction (Substitution' Term)
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
i Type'' Term Term
t IsWithFunction (Substitution' Term)
sub SpineClause
cl TCM a
ret = do
  clo <- () -> TCMT IO (Closure ())
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure ()
  localTC (set eClause (IPClause name i t sub cl clo)) ret