{-# 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 (Semigroup((<>)))

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'(..), 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 )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )

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

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

checkFunDef :: A.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef :: DefInfo -> QName -> [Clause' LHS] -> TCM ()
checkFunDef DefInfo
i QName
name [Clause' LHS]
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
        Definition
def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
        let t :: Type
t    = Definition -> Type
defType Definition
def
        let info :: ArgInfo
info = Definition -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Definition
def

        -- If the function is erased, then hard compile-time mode is
        -- entered.
        ArgInfo -> TCM () -> TCM ()
forall q a. LensQuantity q => q -> TCM a -> TCM a
setHardCompileTimeModeIfErased' ArgInfo
info (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        case [Clause' LHS] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause' LHS]
cs Type
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 -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef, DefInfo -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo
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 -> QName -> [Clause' LHS] -> Bool -> Call
CheckFunDefCall (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
name [Clause' LHS]
cs 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
                  [MetaId]
xs <- Type -> [MetaId]
forall a. AllMetas a => a -> [MetaId]
allMetasList (Type -> [MetaId])
-> (MetaVariable -> Type) -> MetaVariable -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
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
                  (MetaId -> TCM ()) -> [MetaId] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ MetaId -> TCM ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta (MetaId
x MetaId -> [MetaId] -> [MetaId]
forall a. a -> [a] -> [a]
: [MetaId]
xs)
                Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
checkAlias Type
t ArgInfo
info DefInfo
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 -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange DefInfo
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 -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo
i)
              Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause' LHS]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing Maybe QName
forall a. Maybe a
Nothing DefInfo
i QName
name [Clause' LHS]
cs
          Maybe (Expr, Maybe Expr, MetaId)
_ -> Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause' LHS]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing Maybe QName
forall a. Maybe a
Nothing DefInfo
i QName
name [Clause' LHS]
cs

        -- If it's a macro check that it ends in Term → TC ⊤
        let ismacro :: Bool
ismacro = Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> Definition -> Bool
forall a b. (a -> b) -> a -> b
$ Definition
def
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
ismacro Bool -> Bool -> Bool
|| DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM ()
checkMacroType Type
t
    TCM () -> ((TCErr, 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 -> QName -> [Clause' LHS] -> TCErr -> Constraint
CheckFunDef DefInfo
i QName
name [Clause' LHS]
cs TCErr
err

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

  let telList :: [Dom ([Char], Type)]
telList = Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
      resType :: Type
resType = Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract ([Dom ([Char], Type)] -> Tele (Dom Type)
telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. Int -> [a] -> [a]
drop ([Dom ([Char], Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type)]
telList Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Dom ([Char], Type)]
telList)) Type
tr
  Type
expectedType <- TCMT IO Term -> TCMT IO Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCMT IO Type -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCMT IO Term -> TCMT IO Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
resType Type
expectedType
    TCM () -> (TCErr -> TCM ()) -> TCM ()
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`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 -> TypeError
MacroResultTypeMismatch Type
expectedType

-- | A single clause without arguments and without type signature is an alias.
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias :: [Clause' LHS] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause' LHS]
cs Type
t =
        case [Clause' LHS] -> Maybe (Expr, Maybe Expr)
trivialClause [Clause' LHS]
cs of
          -- if we have just one clause without pattern matching and
          -- without a type signature, then infer, to allow
          -- "aliases" for things starting with hidden abstractions
          Just (Expr
e, Maybe Expr
mc) | Just MetaId
x <- Term -> Maybe MetaId
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) -> (Expr, Maybe Expr, MetaId) -> Maybe (Expr, Maybe Expr, MetaId)
forall a. a -> Maybe a
Just (Expr
e, Maybe Expr
mc, MetaId
x)
          Maybe (Expr, Maybe Expr)
_ -> Maybe (Expr, Maybe Expr, MetaId)
forall a. Maybe a
Nothing
  where
    isMeta :: Term -> Maybe MetaId
isMeta (MetaV MetaId
x Elims
_) = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x
    isMeta Term
_           = Maybe MetaId
forall a. Maybe a
Nothing
    trivialClause :: [Clause' LHS] -> 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 Bool
_]
      | 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' LHS]
_ = 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 -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
checkAlias Type
t ArgInfo
ai DefInfo
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 -> ExpandedEllipsis -> LHSInfo
LHSInfo (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) ExpandedEllipsis
NoEllipsis) QName
name []
                        , clauseStrippedPats :: [ProblemEq]
clauseStrippedPats = []
                        , clauseRHS :: RHS
clauseRHS          = Expr -> Maybe Expr -> RHS
A.RHS Expr
e Maybe Expr
mc
                        , clauseWhereDecls :: WhereDeclarations
clauseWhereDecls   = WhereDeclarations
A.noWhereDecls
                        , clauseCatchall :: Bool
clauseCatchall     = Bool
False } in
  QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM ()
-> TCM ()
forall a.
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
0 Type
t Maybe Substitution
forall a. Maybe a
Nothing 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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.
  Term
v <- ArgInfo -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCMT IO Term
checkDontExpandLast Comparison
CmpLeq Expr
e Type
t

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.alias" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkAlias: finished checking"

  DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty

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

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

  -- Add the definition
  FunctionData
fun <- TCMT IO FunctionData
forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
  QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
ai QName
name Type
t (Defn -> TCM ()) -> Defn -> TCM ()
forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn (FunctionData -> Defn) -> FunctionData -> Defn
forall a b. (a -> b) -> a -> b
$
    Lens' FunctionData Bool -> LensSet FunctionData Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> FunctionData -> f FunctionData
Lens' FunctionData Bool
funMacro_ (DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (FunctionData -> FunctionData) -> FunctionData -> FunctionData
forall a b. (a -> b) -> a -> b
$
    Lens' FunctionData IsAbstract -> LensSet FunctionData IsAbstract
forall o i. Lens' o i -> LensSet o i
set (IsAbstract -> f IsAbstract) -> FunctionData -> f FunctionData
Lens' FunctionData IsAbstract
funAbstr_ (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i) (FunctionData -> FunctionData) -> FunctionData -> FunctionData
forall a b. (a -> b) -> a -> b
$
      FunctionData
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    = False
              , clauseExact       = Just True
              , clauseRecursive   = Nothing   -- we don't know yet
              , clauseUnreachable = Just False
              , clauseEllipsis    = NoEllipsis
              , clauseWhereModule = Nothing
              } ]
          , _funCompiled  = Just $ Done [] $ 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 DefInfo -> IsInstance
forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
    InstanceDef KwRange
_r -> 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
$ QName -> Type -> TCM ()
addTypedInstance QName
name Type
t
      -- Put highlighting on the name only;
      -- @(getRange (r, name))@ does not give good results.
    IsInstance
NotInstanceDef -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.alias" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkAlias: leaving"


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

-- | Type check a definition by pattern matching.
checkFunDefS :: Type             -- ^ the type we expect the function to have
             -> ArgInfo          -- ^ is it irrelevant (for instance)
             -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
                                 --   (if so, we need to know some stuff about lambda-lifted args)
             -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
             -> A.DefInfo        -- ^ range info
             -> QName            -- ^ the name of the function
             -> Maybe (Substitution, Map Name LetBinding)
                                 -- ^ substitution (from with abstraction) that needs to be applied
                                 --   to module parameters, and let-bindings inherited from parent
                                 --   clause
             -> [A.Clause]       -- ^ the clauses to check
             -> TCM ()
checkFunDefS :: Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe (Substitution, Map Name LetBinding)
-> [Clause' LHS]
-> TCM ()
checkFunDefS Type
t ArgInfo
ai Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name Maybe (Substitution, Map Name LetBinding)
withSubAndLets [Clause' LHS]
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 -> QName -> [Clause' LHS] -> Bool -> Call
CheckFunDefCall (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
name [Clause' LHS]
cs 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> TCMT IO Doc)
-> (Definition -> Type) -> Definition -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
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 => 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' LHS -> TCMT IO Doc) -> [Clause' LHS] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (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' LHS -> TCMT IO Doc) -> Clause' LHS -> 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' LHS -> [Char]) -> Clause' LHS -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' LHS -> [Char]
forall a. Show a => a -> [Char]
show (Clause' LHS -> [Char])
-> (Clause' LHS -> Clause' LHS) -> Clause' LHS -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' LHS -> Clause' LHS
forall a. ExprLike a => a -> a
A.deepUnscope) [Clause' LHS]
cs

        [SpineClause]
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' LHS -> SpineClause) -> [Clause' LHS] -> [SpineClause]
forall a b. (a -> b) -> [a] -> [b]
map Clause' LHS -> SpineClause
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine [Clause' LHS]
cs

        [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
"spine clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (SpineClause -> TCMT IO Doc) -> [SpineClause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (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)
-> (SpineClause -> TCMT IO Doc) -> SpineClause -> 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)
-> (SpineClause -> [Char]) -> SpineClause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpineClause -> [Char]
forall a. Show a => a -> [Char]
show (SpineClause -> [Char])
-> (SpineClause -> SpineClause) -> SpineClause -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpineClause -> SpineClause
forall a. ExprLike a => a -> a
A.deepUnscope) [SpineClause]
cs

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

        -- Check the clauses
        [(Clause, ClausesPostChecks)]
cs <- Call
-> TCMT IO [(Clause, ClausesPostChecks)]
-> TCMT IO [(Clause, ClausesPostChecks)]
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
NoHighlighting (TCMT IO [(Clause, ClausesPostChecks)]
 -> TCMT IO [(Clause, ClausesPostChecks)])
-> TCMT IO [(Clause, ClausesPostChecks)]
-> TCMT IO [(Clause, ClausesPostChecks)]
forall a b. (a -> b) -> a -> b
$ do -- To avoid flicker.
          [(SpineClause, Int)]
-> ((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO [(Clause, ClausesPostChecks)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([SpineClause] -> [Int] -> [(SpineClause, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SpineClause]
cs [Int
0..]) (((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
 -> TCMT IO [(Clause, ClausesPostChecks)])
-> ((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO [(Clause, ClausesPostChecks)]
forall a b. (a -> b) -> a -> b
$ \ (SpineClause
c, Int
clauseNo) -> do
            QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
clauseNo Type
t ((Substitution, Map Name LetBinding) -> Substitution
forall a b. (a, b) -> a
fst ((Substitution, Map Name LetBinding) -> Substitution)
-> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Substitution, Map Name LetBinding)
withSubAndLets) 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
              (Clause
c,ClausesPostChecks
b) <- ArgInfo
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO (Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
                Type
-> Maybe (Substitution, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe (Substitution, Map Name LetBinding)
withSubAndLets 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.
              Maybe ExtLamInfo -> TCM () -> TCM ()
forall m a. Monoid m => Maybe a -> m -> m
whenNothing Maybe ExtLamInfo
extlam (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty
              -- Andreas, 2013-10-27 add clause as soon it is type-checked
              -- TODO: instantiateFull?
              TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> TCM ()
forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
name [Clause
c]
              (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
c,ClausesPostChecks
b)

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

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

        Bool
canBeSystem <- do
          -- allow VarP and ConP i0/i1 fallThrough = yes, DotP
          let pss :: [[NamedArg DeBruijnPattern]]
pss = (Clause -> [NamedArg DeBruijnPattern])
-> [Clause] -> [[NamedArg DeBruijnPattern]]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> [NamedArg DeBruijnPattern]
namedClausePats [Clause]
cs
              allowed :: Pattern' x -> Bool
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
          Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$! (NamedArg DeBruijnPattern -> Bool)
-> [NamedArg DeBruijnPattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DeBruijnPattern -> Bool
forall {x}. Pattern' x -> Bool
allowed (DeBruijnPattern -> Bool)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) ([[NamedArg DeBruijnPattern]] -> [NamedArg DeBruijnPattern]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NamedArg DeBruijnPattern]]
pss)
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
canBeSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"no pattern matching or path copatterns in systems!"


        [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 (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
$ do
          [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
"checked 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]
map (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]
cs

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

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Int
25 (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
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"clauses before injectivity test"
              , 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
$ [QNamed Clause] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QNamed Clause] -> m Doc
prettyTCM ([QNamed Clause] -> TCMT IO Doc) -> [QNamed Clause] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> QNamed Clause) -> [Clause] -> [QNamed Clause]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs  -- broken, reify (QNamed n cl) expect cl to live at top level
              ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Int
60 (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
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"raw clauses: "
              , 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
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([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
. QNamed Clause -> [Char]
forall a. Show a => a -> [Char]
show (QNamed Clause -> [Char])
-> (Clause -> QNamed Clause) -> Clause -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs
              ]

        -- Needed to calculate the proper fullType below.
        ArgInfo -> TCM () -> TCM ()
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext ArgInfo
ai (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

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

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

        -- Inline copattern record constructors on demand.
        [Clause]
cs <- [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> TCMT IO [[Clause]] -> TCMT IO [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          [Clause] -> (Clause -> TCMT IO [Clause]) -> TCMT IO [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Clause]
cs ((Clause -> TCMT IO [Clause]) -> TCMT IO [[Clause]])
-> (Clause -> TCMT IO [Clause]) -> TCMT IO [[Clause]]
forall a b. (a -> b) -> a -> b
$ \ Clause
cl -> do
            ([Clause]
cls, Bool
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
            Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
nonExactSplit do
              -- If we inlined a non-eta constructor,
              -- issue a warning that the clause does not hold as definitional equality.
              Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> Warning
InlineNoExactSplit QName
name Clause
cl
            [Clause] -> TCMT IO [Clause]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Clause]
cls

        -- 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.
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.def" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checkFunDef': checking injectivity..."
        FunctionInverse
inv <- Account (BenchPhase (TCMT IO))
-> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Injectivity] (TCMT IO FunctionInverse -> TCMT IO FunctionInverse)
-> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
forall a b. (a -> b) -> a -> b
$
          QName -> [Clause] -> TCMT IO FunctionInverse
checkInjectivity QName
name [Clause]
cs

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Int
15 (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
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"clauses before compilation"
              , 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
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QNamed Clause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM (QNamed Clause -> TCMT IO Doc)
-> (Clause -> QNamed Clause) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs
              ]

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc.raw" Int
65 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"clauses before compilation"
              , 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
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([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]
cs
              ]

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

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc.type" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  type   : " 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 ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) Type
t
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc.type" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  context: " 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 ([Char] -> TCMT IO Doc)
-> (Tele (Dom Type) -> [Char]) -> Tele (Dom Type) -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)

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

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

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

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

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Int
60 (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
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"compiled clauses 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
$ CompiledClauses -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty CompiledClauses
cc
              ]

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

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

        -- Add the definition
        TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
name (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do

          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.fun.clauses" Int
15 (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
$ do
            [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"final clauses for" 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 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>  TCMT IO Doc
":"
                 , 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
$ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QNamed Clause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM (QNamed Clause -> TCMT IO Doc)
-> (Clause -> QNamed Clause) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
name) [Clause]
cs
                 ]

          -- If there was a pragma for this definition, we can set the
          -- funTerminates field directly.
          FunctionData
fun  <- TCMT IO FunctionData
forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
          Defn
defn <- Defn -> TCM Defn
autoInline (Defn -> TCM Defn) -> Defn -> TCM Defn
forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn (FunctionData -> Defn) -> FunctionData -> Defn
forall a b. (a -> b) -> a -> b
$
           Lens' FunctionData Bool -> LensSet FunctionData Bool
forall o i. Lens' o i -> LensSet o i
set (Bool -> f Bool) -> FunctionData -> f FunctionData
Lens' FunctionData Bool
funMacro_ (Bool
ismacro Bool -> Bool -> Bool
|| DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
Info.defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
MacroDef) (FunctionData -> FunctionData) -> FunctionData -> FunctionData
forall a b. (a -> b) -> a -> b
$
           Lens' FunctionData IsAbstract -> LensSet FunctionData IsAbstract
forall o i. Lens' o i -> LensSet o i
set (IsAbstract -> f IsAbstract) -> FunctionData -> f FunctionData
Lens' FunctionData IsAbstract
funAbstr_ (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i) (FunctionData -> FunctionData) -> FunctionData -> FunctionData
forall a b. (a -> b) -> a -> b
$
           FunctionData
fun
             { _funClauses        = cs
             , _funCompiled       = Just cc
             , _funSplitTree      = mst
             , _funInv            = inv
             , _funOpaque         = Info.defOpaque i
             , _funExtLam         = (\ ExtLamInfo
e -> ExtLamInfo
e { extLamSys = sys }) <$> extlam
             , _funWith           = with
             , _funCovering       = covering
             }
          Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
          Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$
            (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
forall a b. a -> b -> a
const (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Bool
hasProjectionPatterns CompiledClauses
cc) (Definition -> Definition) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$
            (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
ai QName
name Type
fullType Language
lang Defn
defn)

        [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
$ do
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"added " 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 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , 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
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> TCMT IO Doc)
-> (Definition -> Type) -> Definition -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
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 => QName -> m Definition
getConstInfo QName
name
              ]

        -- Jesper, 2019-05-30: if the constructors used in the
        -- lhs of a clause have rewrite rules, we need to check
        -- confluence here
        TCMT IO (Maybe ConfluenceCheck)
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \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
  TerminationCheck ()
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 :: Maybe Bool
terminates = case TerminationCheck ()
tc of
        TerminationCheck ()
NonTerminating -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        TerminationCheck ()
Terminating    -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        TerminationCheck ()
_              -> Maybe Bool
forall a. Maybe a
Nothing
  [Char] -> Int -> [[Char]] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"tc.fundef" Int
30 ([[Char]] -> TCM ()) -> [[Char]] -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"funTerminates of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" set to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Bool -> [Char]
forall a. Show a => a -> [Char]
show Maybe Bool
terminates
    , [Char]
"  tc = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TerminationCheck () -> [Char]
forall a. Show a => a -> [Char]
show TerminationCheck ()
tc
    ]
  Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ Definition
def { theDef = 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 of the given RHS.
-- (Used to insert patterns for @rewrite@ or the inspect idiom)
mapLHSCores :: (A.LHSCore -> A.LHSCore) -> (A.RHS -> A.RHS)
mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f = \case
  A.WithRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
cs -> QName -> [WithExpr] -> List1 (Clause' LHS) -> RHS
A.WithRHS QName
aux [WithExpr]
es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
forall a b. (a -> b) -> a -> b
$ List1 (Clause' LHS)
-> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for List1 (Clause' LHS)
cs ((Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS))
-> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
forall a b. (a -> b) -> a -> b
$
    \ (A.Clause (A.LHS LHSInfo
info LHSCore' Expr
core)     [ProblemEq]
spats RHS
rhs                 WhereDeclarations
ds Bool
catchall) ->
       LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
info (LHSCore' Expr -> LHSCore' Expr
f LHSCore' Expr
core)) [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f RHS
rhs) WhereDeclarations
ds Bool
catchall
  A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
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

-- | Insert some names into the with-clauses LHS of the given RHS.
-- (Used for the inspect idiom)
insertNames :: [Arg (Maybe A.BindName)] -> A.RHS -> A.RHS
insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS
insertNames = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS)
-> ([Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr)
-> [Arg (Maybe BindName)]
-> RHS
-> RHS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects

insertInspects :: [Arg (Maybe A.BindName)] -> A.LHSCore -> A.LHSCore
insertInspects :: [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects [Arg (Maybe BindName)]
ps = \case
  A.LHSWith LHSCore' Expr
core [Arg (Pattern' Expr)]
wps [] ->
    let ps' :: [Arg (Maybe (Arg (Pattern' Expr)))]
ps' = (Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
-> [Arg (Maybe BindName)] -> [Arg (Maybe (Arg (Pattern' Expr)))]
forall a b. (a -> b) -> [a] -> [b]
map ((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) [Arg (Maybe BindName)]
ps in
    LHSCore' Expr
-> [Arg (Pattern' Expr)]
-> [NamedArg (Pattern' Expr)]
-> LHSCore' Expr
forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core ([Arg (Maybe (Arg (Pattern' Expr)))]
-> [Arg (Pattern' Expr)] -> [Arg (Pattern' Expr)]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg (Pattern' Expr)))]
ps' [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]
: ([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Arg a -> [Arg a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 =
          ([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Arg a -> [Arg a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 :: [Arg A.Pattern] -> A.RHS -> A.RHS
insertPatterns :: [Arg (Pattern' Expr)] -> RHS -> RHS
insertPatterns [Arg (Pattern' Expr)]
pats = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores ([Arg (Pattern' Expr)] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Arg (Pattern' Expr)]
pats)

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

-- | Parameters for creating a @with@-function.
data WithFunctionProblem
  = NoWithFunction
  | WithFunction
    { WithFunctionProblem -> QName
wfParentName :: QName                             -- ^ Parent function name.
    , WithFunctionProblem -> QName
wfName       :: QName                             -- ^ With function name.
    , WithFunctionProblem -> Type
wfParentType :: Type                              -- ^ Type of the parent function.
    , WithFunctionProblem -> Tele (Dom Type)
wfParentTel  :: Telescope                         -- ^ Context of the parent patterns.
    , WithFunctionProblem -> Tele (Dom Type)
wfBeforeTel  :: Telescope                         -- ^ Types of arguments to the with function before the with expressions (needed vars).
    , WithFunctionProblem -> Tele (Dom Type)
wfAfterTel   :: Telescope                         -- ^ Types of arguments to the with function after the with expressions (unneeded vars).
    , WithFunctionProblem -> [Arg (Term, EqualityView)]
wfExprs      :: [Arg (Term, EqualityView)]        -- ^ With and rewrite expressions and their types.
    , WithFunctionProblem -> Type
wfRHSType    :: Type                              -- ^ Type of the right hand side.
    , WithFunctionProblem -> [NamedArg DeBruijnPattern]
wfParentPats :: [NamedArg DeBruijnPattern]        -- ^ Parent patterns.
    , WithFunctionProblem -> Int
wfParentParams :: Nat                             -- ^ Number of module parameters in parent patterns
    , WithFunctionProblem -> Permutation
wfPermSplit  :: Permutation                       -- ^ Permutation resulting from splitting the telescope into needed and unneeded vars.
    , WithFunctionProblem -> Permutation
wfPermParent :: Permutation                       -- ^ Permutation reordering the variables in the parent pattern.
    , WithFunctionProblem -> Permutation
wfPermFinal  :: Permutation                       -- ^ Final permutation (including permutation for the parent clause).
    , WithFunctionProblem -> List1 (Clause' LHS)
wfClauses    :: List1 A.Clause                    -- ^ The given clauses for the with function
    , WithFunctionProblem -> Substitution
wfCallSubst :: Substitution                       -- ^ Subtsitution to generate call for the parent.
    , WithFunctionProblem -> 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 -> [Clause] -> TCMT IO System
checkSystemCoverage QName
f [Int
n] Type
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
  TelV Tele (Dom Type)
gamma Type
t <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
n Type
t
  Tele (Dom Type) -> TCMT IO System -> TCMT IO System
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (TCMT IO System -> TCMT IO System)
-> TCMT IO System -> TCMT IO System
forall a b. (a -> b) -> a -> b
$ do
  TelV (ExtendTel Dom Type
a Abs (Tele (Dom Type))
_) Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
1 Type
t
  Term
a <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a

  case Term
a of
    Def QName
q [Apply Arg Term
phi] -> do
      [Maybe QName
iz,Maybe QName
io] <- (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]
      Term
ineg <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
      Term
imin <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
      Term
imax <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
      Term
i0 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      Term
i1 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
      let
        isDir :: DeBruijnPattern -> Maybe Bool
isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
iz = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
io = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        isDir DeBruijnPattern
_ = Maybe Bool
forall a. Maybe a
Nothing

        collectDirs :: [Int] -> [DeBruijnPattern] -> [(Int,Bool)]
        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, 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] -> 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] -> Term
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 :: [[DeBruijnPattern]]
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 :: [[(Int, Bool)]]
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 :: [Term]
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
psi = [Term] -> Term
orI ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
phis
        pcs :: [(Term, Clause)]
pcs = [Term] -> [Clause] -> [(Term, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
phis [Clause]
cs

      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sys.cover" 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
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ([DeBruijnPattern] -> TCMT IO Doc)
-> [[DeBruijnPattern]] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map [DeBruijnPattern] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
prettyTCM [[DeBruijnPattern]]
pats
      Type
interval <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
      [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
$ TCMT IO Doc
"equalTerm " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
psi
      Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
interval (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi) Term
psi

      [[(Term, Clause)]] -> ([(Term, Clause)] -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([[(Term, Clause)]] -> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a. [a] -> [a] -> [a]
initWithDefault [[(Term, Clause)]]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([[(Term, Clause)]] -> [[(Term, Clause)]])
-> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a b. (a -> b) -> a -> b
$
             [[(Term, Clause)]] -> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a. [a] -> [a] -> [a]
initWithDefault [[(Term, Clause)]]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([[(Term, Clause)]] -> [[(Term, Clause)]])
-> [[(Term, Clause)]] -> [[(Term, Clause)]]
forall a b. (a -> b) -> a -> b
$ [(Term, Clause)] -> [[(Term, Clause)]]
forall a. [a] -> [[a]]
List.tails [(Term, Clause)]
pcs) (([(Term, Clause)] -> TCM ()) -> TCM ())
-> ([(Term, Clause)] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ ((Term
phi1,Clause
cl1):[(Term, Clause)]
pcs') -> do
        [(Term, Clause)] -> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Term, Clause)]
pcs' (((Term, Clause) -> TCMT IO [()]) -> TCM ())
-> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
phi2,Clause
cl2) -> do
          Term
phi12 <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
imin Term -> [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])
          Term
-> (IntMap Bool -> Blocker -> Term -> TCM ())
-> (IntMap Bool -> Substitution -> TCM ())
-> TCMT IO [()]
forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (IntMap Bool -> Blocker -> Term -> m a)
-> (IntMap Bool -> Substitution -> m a)
-> m [a]
forallFaceMaps Term
phi12 (\ IntMap Bool
_ Blocker
_ -> Term -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__) ((IntMap Bool -> Substitution -> TCM ()) -> TCMT IO [()])
-> (IntMap Bool -> Substitution -> TCM ()) -> TCMT IO [()]
forall a b. (a -> b) -> a -> b
$ \IntMap Bool
_ Substitution
sigma -> do
            let args :: [Arg Term]
args = Substitution
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) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
                t' :: Type
t' = Substitution
Substitution' (SubstArg Type)
sigma Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
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 Tele (Dom Type)
delta Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
extra Type
t'
                  (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
delta) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Term -> TCMT IO Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
                    (Reduced (Blocked' Term Term) Term -> Term)
-> TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reduced (Blocked' Term Term) Term -> Term
forall {t} {yes}. Reduced (Blocked' t yes) yes -> yes
fromReduced (TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term)
-> TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ReduceM (Reduced (Blocked' Term Term) Term)
-> TCMT IO (Reduced (Blocked' Term Term) Term)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Reduced (Blocked' Term Term) Term)
 -> TCMT IO (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> TCMT IO (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$
                      QName
-> Term
-> [Clause]
-> RewriteRules
-> MaybeReducedArgs
-> ReduceM (Reduced (Blocked' Term Term) Term)
appDef' QName
f (QName -> Elims -> Term
Def QName
f []) [Clause
cl] [] ((Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced ([Arg Term] -> MaybeReducedArgs) -> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) [Arg Term]
args [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
delta)
            Term
v1 <- Clause -> TCMT IO Term
body Clause
cl1
            Term
v2 <- Clause -> TCMT IO Term
body Clause
cl2
            Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t' Term
v1 Term
v2

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

            let
                -- Δ = Γ_α , Δ'α
                delta :: Tele (Dom Type)
delta = Clause -> Tele (Dom Type)
clauseTel Clause
cl
                -- Δ ⊢ b
                Just Term
b = Clause -> Maybe Term
clauseBody Clause
cl
                -- Δ ⊢ ps : Γ , o : [φ] , Δ'
                -- we assume that there's no pattern matching other
                -- than from the system
                ps :: [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) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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)
tel = [Dom ([Char], Type)] -> Tele (Dom Type)
telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. Int -> [a] -> [a]
takeLast Int
extra (Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
delta))
                u :: Term
u = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
extra ([Int] -> Substitution
forall {a}.
(SubstArg a ~ a, Subst a, DeBruijn a) =>
[Int] -> Substitution' a
weak ([Int] -> Substitution) -> [Int] -> Substitution
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)

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


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

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

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

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

-- | The LHS part of checkClause.
checkClauseLHS :: Type -> Maybe Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClauseLHS :: forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
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 Bool
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)]
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
trailingWithPatterns [NamedArg (Pattern' Expr)]
aps) (([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ())
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [NamedArg (Pattern' Expr)]
withPats -> do
      TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Pattern' Expr] -> TypeError
UnexpectedWithPatterns ([Pattern' Expr] -> TypeError) -> [Pattern' Expr] -> TypeError
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> Pattern' Expr)
-> [NamedArg (Pattern' Expr)] -> [Pattern' Expr]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg [NamedArg (Pattern' Expr)]
withPats
    Call -> TCM a -> TCM a
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Type -> SpineClause -> Call
CheckClause Type
t SpineClause
c) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
      [NamedArg (Pattern' Expr)]
aps <- [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg (Pattern' Expr)]
aps
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ProblemEq] -> Bool
forall a. Null a => a -> Bool
null [ProblemEq]
strippedPats) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"strippedPats:" 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 [ Pattern' Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern' Expr
p 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
<+> 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
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a | A.ProblemEq Pattern' Expr
p Term
v Dom Type
a <- [ProblemEq]
strippedPats ]
      Type
closed_t <- (Tele (Dom Type) -> Type -> Type)
-> Type -> Tele (Dom Type) -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Type
t (Tele (Dom Type) -> Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      Call
-> Range
-> Maybe QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
forall a.
Call
-> Range
-> Maybe QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide (SpineLHS -> Call
CheckLHS SpineLHS
lhs) (SpineLHS -> Range
forall a. HasRange a => a -> Range
getRange SpineLHS
lhs) (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x) [NamedArg (Pattern' Expr)]
aps Type
t Maybe Substitution
withSub [ProblemEq]
strippedPats LHSResult -> TCM a
ret

-- | Type check a function clause.

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

checkClause :: Type
-> Maybe (Substitution, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe (Substitution, 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 Bool
catchall) = do
  let withSub :: Maybe Substitution
withSub       = (Substitution, Map Name LetBinding) -> Substitution
forall a b. (a, b) -> a
fst ((Substitution, Map Name LetBinding) -> Substitution)
-> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Substitution, Map Name LetBinding)
withSubAndLets
  [Name]
cxtNames <- [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name])
-> ([Dom' Term (Name, Type)] -> [Name])
-> [Dom' Term (Name, Type)]
-> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term (Name, Type) -> Name)
-> [Dom' Term (Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Name])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
  Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
withSub SpineClause
c ((LHSResult -> TCMT IO (Clause, ClausesPostChecks))
 -> TCMT IO (Clause, ClausesPostChecks))
-> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ \ lhsResult :: LHSResult
lhsResult@(LHSResult Int
npars Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg Type
trhs Substitution
patSubst [AsBinding]
asb IntSet
psplit Bool
ixsplit) -> do

    let installInheritedLets :: TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
installInheritedLets TCMT IO (Clause, ClausesPostChecks)
k
          | Just (Substitution
withSub, Map Name LetBinding
lets) <- Maybe (Substitution, Map Name LetBinding)
withSubAndLets = do
            Map Name (Open LetBinding)
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
patSubst Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
withSub) Map Name LetBinding
lets
            Lens' TCEnv (Map Name (Open LetBinding))
-> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings (Map Name (Open LetBinding)
lets' Map Name (Open LetBinding)
-> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall a. Semigroup a => a -> a -> a
<>) TCMT IO (Clause, ClausesPostChecks)
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.
        Type
t' <- case Maybe Substitution
withSub of
                Just{}  -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
                Maybe Substitution
Nothing -> do
                  Tele (Dom Type)
theta <- ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (QName -> ModuleName
qnameModule QName
x)
                  Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
theta Type
t

        -- At this point we should update the named dots potential with-clauses
        -- in the right-hand side. When checking a clause we expect the named
        -- dots to live in the context of the closest parent lhs, but the named
        -- dots added by buildWithFunction live in the context of the
        -- with-function arguments before pattern matching. That's what we need
        -- patSubst for.
        let rhs :: RHS
rhs = RHS -> RHS
updateRHS RHS
rhs0
            updateRHS :: RHS -> RHS
updateRHS rhs :: RHS
rhs@A.RHS{}               = RHS
rhs
            updateRHS rhs :: RHS
rhs@A.AbsurdRHS{}         = RHS
rhs
            updateRHS (A.WithRHS QName
q [WithExpr]
es List1 (Clause' LHS)
cs)       = QName -> [WithExpr] -> List1 (Clause' LHS) -> RHS
A.WithRHS QName
q [WithExpr]
es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
forall a b. (a -> b) -> a -> b
$ (Clause' LHS -> Clause' LHS)
-> List1 (Clause' LHS) -> List1 (Clause' LHS)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause' LHS -> Clause' LHS
updateClause List1 (Clause' LHS)
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
Substitution' (SubstArg [ProblemEq])
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh

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

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

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

        Maybe Term
wbody <- TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
-> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Account (BenchPhase (TCMT IO))
-> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
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] (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
-> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ [Name] -> WithFunctionProblem -> TCMT IO (Maybe Term)
checkWithFunction [Name]
cxtNames WithFunctionProblem
with

        Maybe Term
body <- Maybe Term -> TCMT IO (Maybe Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCMT IO (Maybe Term))
-> Maybe Term -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Maybe Term
body Maybe Term -> Maybe Term -> Maybe Term
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe Term
wbody

        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optDoubleCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Maybe Term
body of
          Just Term
v  -> do
            [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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs))
              ]
            TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(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 (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
a -> Comparison -> TypeOf a -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> TypeOf Term -> m ()
checkInternal Term
v Comparison
CmpLeq (TypeOf Term -> TCM ()) -> TypeOf Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs
          Maybe Term
Nothing -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.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
"Clause before translation:"
          , 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
"delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta
            , TCMT IO Doc
"ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> TCMT IO [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern]
ps
            , TCMT IO Doc
"body  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> (Term -> TCMT IO Doc) -> Maybe Term -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"_|_" Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Maybe Term
body
            , TCMT IO Doc
"type  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
            ]
          ]

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (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
"Clause before translation (raw):"
          , 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
"ps    =" 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 ([NamedArg DeBruijnPattern] -> [Char]
forall a. Show a => a -> [Char]
show [NamedArg DeBruijnPattern]
ps)
            , TCMT IO Doc
"body  =" 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 (Maybe Term -> [Char]
forall a. Show a => a -> [Char]
show Maybe Term
body)
            , TCMT IO Doc
"type  =" 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 (Type -> [Char]
forall a. Show a => a -> [Char]
show Type
t)
            ]
          ]

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

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

        -- absurd clauses are not exact
        let exact :: Maybe Bool
exact = if Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
body then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False else Maybe Bool
forall a. Maybe a
Nothing -- we don't know yet

        (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Clause, ClausesPostChecks)
 -> TCMT IO (Clause, ClausesPostChecks))
-> (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ (, IntSet -> ClausesPostChecks
CPC IntSet
psplit)
          Clause { clauseLHSRange :: Range
clauseLHSRange  = LHSInfo -> Range
forall a. HasRange a => a -> Range
getRange LHSInfo
i
                 , clauseFullRange :: Range
clauseFullRange = SpineClause -> Range
forall a. HasRange a => a -> Range
getRange SpineClause
c
                 , clauseTel :: Tele (Dom Type)
clauseTel       = KillRangeT (Tele (Dom Type))
forall a. KillRange a => KillRangeT a
killRange Tele (Dom Type)
delta
                 , namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps
                 , clauseBody :: Maybe Term
clauseBody      = Maybe Term -> Maybe Term
bodyMod Maybe Term
body
                 , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just Arg Type
trhs
                 , clauseCatchall :: Bool
clauseCatchall  = Bool
catchall'
                 , clauseExact :: Maybe Bool
clauseExact       = Maybe Bool
exact
                 , clauseRecursive :: Maybe Bool
clauseRecursive   = Maybe Bool
forall a. Maybe a
Nothing -- we don't know yet
                 , clauseUnreachable :: Maybe Bool
clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing -- we don't know yet
                 , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = LHSInfo -> ExpandedEllipsis
lhsEllipsis LHSInfo
i
                 , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = WhereDeclarations -> Maybe ModuleName
A.whereModule WhereDeclarations
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 ConHead
reflCon ConInfo
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl

  Maybe ArgInfo
reflInfo <- (ArgInfo -> ArgInfo) -> Maybe ArgInfo -> Maybe ArgInfo
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) (Maybe ArgInfo -> Maybe ArgInfo)
-> TCMT IO (Maybe ArgInfo) -> TCMT IO (Maybe ArgInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
reflCon
  let patInfo :: ConPatInfo
patInfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager
  -- The REFL constructor might have an argument
  let reflArg :: [NamedArg (Pattern' Expr)]
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

  Pattern' Expr -> TCM (Pattern' Expr)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Expr -> TCM (Pattern' Expr))
-> Pattern' Expr -> TCM (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ ConPatInfo
-> AmbiguousQName -> [NamedArg (Pattern' Expr)] -> Pattern' Expr
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
patInfo (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
reflCon) [NamedArg (Pattern' Expr)]
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
-> LHSResult
-> RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps Type
t lhsResult :: LHSResult
lhsResult@(LHSResult Int
_ Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg Type
trhs Substitution
_ [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 [WithExpr]
es List1 (Clause' LHS)
cs        -> QName
-> [WithExpr]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
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@.
    Maybe Term
mv <- if Bool
absurdPat
          then do
            [NamedArg DeBruijnPattern]
ps <- [NamedArg DeBruijnPattern] -> TCMT IO [NamedArg DeBruijnPattern]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [NamedArg DeBruijnPattern]
ps
            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
<$ Expr -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
e (Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Warning
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
ps)
          else Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> TCMT IO Term -> TCMT IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Type -> TCMT IO Term
checkExpr Expr
e (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs)
    (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
mv, WithFunctionProblem
NoWithFunction)

  -- Absurd case: no right hand side
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
  noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS = do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
absurdPat (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> TypeError
NoRHSRequiresAbsurdPattern [NamedArg (Pattern' Expr)]
aps
    (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing, WithFunctionProblem
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
    -> [A.WithExpr]      -- @[{a} in eqa, b in eqb, {{c}}, ...]@
    -> List1 A.Clause    -- @[(ps1 = rhs1), (ps2 = rhs), ...]@
    -> TCM (Maybe Term, WithFunctionProblem)
  withRHS :: QName
-> [WithExpr]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
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"
      , [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
$ QName -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA QName
aux TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (WithExpr -> TCMT IO Doc) -> [WithExpr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (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) [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
      Int
nfv <- TCM Int
getCurrentModuleFreeVars
      ModuleName
m   <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"with function module:" 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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Name -> TCMT IO Doc) -> [Name] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM ([Name] -> [TCMT IO Doc]) -> [Name] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m)
          ,  [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"free variables: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
nfv
          ]

    -- Infer the types of the with expressions

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

    let names :: [Arg (Maybe BindName)]
names = (WithExpr -> Arg (Maybe BindName))
-> [WithExpr] -> [Arg (Maybe BindName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (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) [WithExpr]
es
    List1 (Clause' LHS)
cs <- List1 (Clause' LHS)
-> (Clause' LHS -> TCMT IO (Clause' LHS))
-> TCMT IO (List1 (Clause' LHS))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 (Clause' LHS)
cs ((Clause' LHS -> TCMT IO (Clause' LHS))
 -> TCMT IO (List1 (Clause' LHS)))
-> (Clause' LHS -> TCMT IO (Clause' LHS))
-> TCMT IO (List1 (Clause' LHS))
forall a b. (a -> b) -> a -> b
$ \ c :: Clause' LHS
c@(A.Clause (A.LHS LHSInfo
i LHSCore' Expr
core) [ProblemEq]
eqs RHS
rhs WhereDeclarations
wh Bool
b) -> do
      let rhs' :: RHS
rhs'  = [Arg (Maybe BindName)] -> RHS -> RHS
insertNames    [Arg (Maybe BindName)]
names RHS
rhs
      let core' :: LHSCore' Expr
core' = [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects [Arg (Maybe BindName)]
names LHSCore' Expr
core
      Clause' LHS -> TCMT IO (Clause' LHS)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause' LHS -> TCMT IO (Clause' LHS))
-> Clause' LHS -> TCMT IO (Clause' LHS)
forall a b. (a -> b) -> a -> b
$ LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i LHSCore' Expr
core') [ProblemEq]
eqs RHS
rhs' WhereDeclarations
wh Bool
b

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

    QName
-> QName
-> Type
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type
t LHSResult
lhsResult [Arg (Term, EqualityView)]
vtys List1 (Clause' LHS)
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
-> [Named BindName (Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname (List1 (Named BindName (Pattern' Expr, Expr))
-> [Item (List1 (Named BindName (Pattern' Expr, Expr)))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Named BindName (Pattern' Expr, Expr))
pes) [RewriteEqn]
rs
    LeftLet List1 (Pattern' Expr, Expr)
pes -> [(Pattern' Expr, Expr)]
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS (List1 (Pattern' Expr, Expr) -> [Item (List1 (Pattern' Expr, Expr))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Pattern' Expr, Expr)
pes) [RewriteEqn]
rs

    where

    -- @using@ clauses
    usingEqnRHS :: [(A.Pattern, A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    usingEqnRHS :: [(Pattern' Expr, Expr)]
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS [(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 ([(Pattern' Expr, Expr)] -> [Item [(Pattern' Expr, Expr)]]
forall l. IsList l => l -> [Item l]
List1.toList [(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 -> Pattern' Expr -> Expr -> LetBinding
A.LetPatBind (Range -> LetInfo
LetRange (Range -> LetInfo) -> Range -> LetInfo
forall a b. (a -> b) -> a -> b
$ Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) 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 -> [Named A.BindName (A.Pattern,A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    invertEqnRHS :: QName
-> [Named BindName (Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname [Named BindName (Pattern' Expr, Expr)]
pes [RewriteEqn]
rs = do

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

      let pats :: [Arg (Pattern' Expr)]
pats = ([Pattern' Expr] -> [Arg (Pattern' Expr)])
-> [[Pattern' Expr]] -> [Arg (Pattern' Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Pattern' Expr -> Arg (Pattern' Expr))
-> [Pattern' Expr] -> [Arg (Pattern' Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg) ([[Pattern' Expr]] -> [Arg (Pattern' Expr)])
-> [[Pattern' Expr]] -> [Arg (Pattern' Expr)]
forall a b. (a -> b) -> a -> b
$
            [Named BindName (Pattern' Expr)]
-> (Named BindName (Pattern' Expr) -> [Pattern' Expr])
-> [[Pattern' Expr]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Named BindName (Pattern' Expr)]
npats ((Named BindName (Pattern' Expr) -> [Pattern' Expr])
 -> [[Pattern' Expr]])
-> (Named BindName (Pattern' Expr) -> [Pattern' Expr])
-> [[Pattern' Expr]]
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Pattern' Expr
p) -> case Maybe BindName
nm of
              Maybe BindName
Nothing -> [Pattern' Expr
p]
              Just BindName
n  -> [Pattern' Expr
p, BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP BindName
n]

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

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

      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.invert" Int
60 (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
        [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"invert"
        , TCMT IO Doc
"  rhs' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (RHS -> [Char]) -> RHS -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RHS -> [Char]
forall a. Show a => a -> [Char]
show) RHS
rhs'
        ]
      QName
-> QName
-> Type
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
qname Type
t LHSResult
lhsResult [Arg (Term, EqualityView)]
vtys (List1 (Clause' LHS) -> TCM (Maybe Term, WithFunctionProblem))
-> List1 (Clause' LHS) -> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ Clause' LHS -> List1 (Clause' LHS)
forall el coll. Singleton el coll => el -> coll
singleton Clause' LHS
cl

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

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

      -- Get value and type of rewrite-expression.

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

      -- Andreas, 2024-02-27, issue #7150
      -- trigger instance search to resolve instances in rewrite-expression
      TCM ()
forall (m :: * -> *). MonadConstraint m => m ()
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.
      DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DefaultToInfty

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

      Type
t' <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
eqt
      (EqualityView
eqt,Type
rewriteType,Term
rewriteFrom,Term
rewriteTo) <- Type -> TCM EqualityView
equalityView Type
t' TCM EqualityView
-> (EqualityView -> TCMT IO (EqualityView, Type, Term, Term))
-> TCMT IO (EqualityView, Type, Term, Term)
forall 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
        eqt :: EqualityView
eqt@(EqualityType Sort
_s QName
_eq [Arg Term]
_params (Arg ArgInfo
_ Term
dom) Arg Term
a Arg Term
b) -> do
          Sort
s <- Term -> TCMT IO Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
dom
          (EqualityView, Type, Term, Term)
-> TCMT IO (EqualityView, Type, Term, Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView
eqt, Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s Term
dom, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b)
          -- Note: the sort _s of the equality need not be the sort of the type @dom@!
        OtherType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
-> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
CannotRewriteByNonEquation Type
t'
        IdiomType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
-> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
CannotRewriteByNonEquation Type
t'

      Pattern' Expr
reflPat <- TCM (Pattern' Expr)
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 :: TCMT IO Bool
isReflexive = TCM () -> TCMT IO Bool
forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
           Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
rewriteType Term
rewriteFrom Term
rewriteTo

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

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

      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rewrite" Int
60 (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
        [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"rewrite"
        , TCMT IO Doc
"  rhs' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (RHS -> [Char]) -> RHS -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RHS -> [Char]
forall a. Show a => a -> [Char]
show) RHS
rhs'
        ]
      QName
-> QName
-> Type
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
qname Type
t LHSResult
lhsResult [(Term, EqualityView) -> Arg (Term, EqualityView)
forall a. a -> Arg a
defaultArg (Term
withExpr, EqualityView
withType)] (List1 (Clause' LHS) -> TCM (Maybe Term, WithFunctionProblem))
-> List1 (Clause' LHS) -> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ Clause' LHS -> List1 (Clause' LHS)
forall el coll. Singleton el coll => el -> coll
singleton Clause' LHS
cl

checkWithRHS
  :: QName                             -- ^ Name of function.
  -> QName                             -- ^ Name of the with-function.
  -> Type                              -- ^ Type of function.
  -> LHSResult                         -- ^ Result of type-checking patterns
  -> [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
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type
t (LHSResult Int
npars Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
_absurdPat Arg Type
trhs Substitution
_ [AsBinding]
_asb IntSet
_ Bool
_) [Arg (Term, EqualityView)]
vtys0 List1 (Clause' LHS)
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
        [Arg Term]
withArgs <- [Arg (Term, EqualityView)] -> TCM [Arg Term]
withArguments [Arg (Term, EqualityView)]
vtys0
        let perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm [NamedArg DeBruijnPattern]
ps

        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
          -- declared locally because we do not want to use the unzip'd thing!
          let ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [Arg (Term, EqualityView)]
vtys0 in
          [ TCMT IO Doc
"vs (before normalization) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
vs
          , TCMT IO Doc
"as (before normalization) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [EqualityView] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [EqualityView] -> m Doc
prettyTCM [EqualityView]
as
          ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
45 (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
$
          -- declared locally because we do not want to use the unzip'd thing!
          let ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [Arg (Term, EqualityView)]
vtys0 in
          [ TCMT IO Doc
"vs (before norm., raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Term]
vs
          ]
        [Arg (Term, EqualityView)]
vtys0 <- [Arg (Term, EqualityView)] -> TCMT IO [Arg (Term, EqualityView)]
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise [Arg (Term, EqualityView)]
vtys0

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (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
"delta  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta
          ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
25 (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
$
          -- declared locally because we do not want to use the unzip'd thing!
          let ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [Arg (Term, EqualityView)]
vtys0 in
          [ TCMT IO Doc
"vs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
vs
          , TCMT IO Doc
"as     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [EqualityView] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [EqualityView] -> m Doc
prettyTCM [EqualityView]
as
          , 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)
          ]

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

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

        -- Andreas, 2012-09-17: for printing delta,
        -- we should remove it from the context first
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (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
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta2)
          ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
25 (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
"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)
          ]

        -- Create the body of the original function

        -- All the context variables
        [Term]
us <- TCMT IO [Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms
        let n :: Int
n = [Term] -> Int
forall a. Sized a => a -> Int
size [Term]
us
            m :: Int
m = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta
            -- First the variables bound outside this definition
            ([Term]
us0, [Term]
us1') = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) [Term]
us
            -- Then permute the rest and grab those needed to for the with arguments
            ([Term]
us1, [Term]
us2)  = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta1) ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ Permutation -> [Term] -> [Term]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm' [Term]
us1'
            -- Now stuff the with arguments in between and finish with the remaining variables
            argsS :: Substitution
argsS = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> [Term] -> Substitution
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 [Arg Term]
withArgs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
us2
            v :: Maybe a
v         = Maybe a
forall a. Maybe a
Nothing -- generated by checkWithFunction
        -- Andreas, 2013-02-26 add with-name to signature for printing purposes
        QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
          Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
aux Type
HasCallStack => Type
__DUMMY_TYPE__ Language
lang (Defn -> Definition) -> TCM Defn -> TCMT IO Definition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              TCM Defn
forall (m :: * -> *). HasOptions m => m Defn
emptyFunction

        [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] -> 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 ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [Arg (Term, EqualityView)]
vtys in
          [ TCMT IO Doc
"    with arguments" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM [Term]
vs)
          , TCMT IO Doc
"             types" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((EqualityView -> TCMT IO Doc) -> [EqualityView] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map EqualityView -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => EqualityView -> m Doc
prettyTCM [EqualityView]
as)
          , TCMT IO Doc
"           context" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)
          , TCMT IO Doc
"             delta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta
          , TCMT IO Doc
"            delta1" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta1
          , TCMT IO Doc
"            delta2" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta2
          ]

        -- Only inherit user-written let bindings from parent clauses. Others, like @-patterns,
        -- should not be carried over.
        Map Name LetBinding
lets <- (LetBinding -> Bool) -> Map Name LetBinding -> Map Name LetBinding
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
UserWritten) (Origin -> Bool) -> (LetBinding -> Origin) -> LetBinding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> Origin
letOrigin) (Map Name LetBinding -> Map Name LetBinding)
-> TCMT IO (Map Name LetBinding) -> TCMT IO (Map Name LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Open LetBinding -> TCMT IO LetBinding)
-> Map Name (Open LetBinding) -> TCMT IO (Map Name 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 Open LetBinding -> TCMT IO LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen (Map Name (Open LetBinding) -> TCMT IO (Map Name LetBinding))
-> TCMT IO (Map Name (Open LetBinding))
-> TCMT IO (Map Name LetBinding)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCEnv (Map Name (Open LetBinding))
-> TCMT IO (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings)

        (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
v, QName
-> QName
-> Type
-> Tele (Dom Type)
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [Arg (Term, EqualityView)]
-> Type
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> Permutation
-> Permutation
-> List1 (Clause' LHS)
-> Substitution
-> Map Name LetBinding
-> WithFunctionProblem
WithFunction QName
x QName
aux Type
t Tele (Dom Type)
delta Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 [Arg (Term, EqualityView)]
vtys Type
t' [NamedArg DeBruijnPattern]
ps Int
npars Permutation
perm' Permutation
perm Permutation
finalPerm List1 (Clause' LHS)
cs Substitution
argsS Map Name LetBinding
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 QName
f QName
aux Type
t Tele (Dom Type)
delta Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 [Arg (Term, EqualityView)]
vtys Type
b [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm' Permutation
perm Permutation
finalPerm List1 (Clause' LHS)
cs Substitution
argsS Map Name LetBinding
lets) = do
  let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
      withSub :: Substitution
      withSub :: Substitution
withSub = let as :: [EqualityView]
as = (Arg (Term, EqualityView) -> EqualityView)
-> [Arg (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((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) [Arg (Term, EqualityView)]
vtys in
                Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta2) (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
wkS ([EqualityView] -> Int
countWithArgs [EqualityView]
as) Substitution
forall a. Substitution' a
idS)
                Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Impossible -> Permutation -> Substitution
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 ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [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) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 ([EqualityView] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [EqualityView] -> m Doc
prettyTCM [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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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) -> 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) -> m a -> m a
addContext Tele (Dom Type)
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 -> [Char]
forall a. Show a => a -> [Char]
show Substitution
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]
  Tele (Dom Type)
delta1 <- (SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
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)) -> TCMT IO (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
delta1

  -- Generate the type of the with function
  (Type
withFunType, Int
n) <- do
    let ps :: [NamedArg DeBruijnPattern]
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
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.bndry" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta2
                                  (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
ps
    let vs :: [Int]
vs = [NamedArg DeBruijnPattern] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg DeBruijnPattern]
ps
    [(Int, (Term, Term))]
bndry <- if [Int] -> Bool
forall a. Null a => a -> Bool
null [Int]
vs then [(Int, (Term, Term))] -> TCMT IO [(Int, (Term, Term))]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
      Term
iz <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      Term
io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
      let tm :: Term
tm = QName -> Elims -> Term
Def QName
f ([NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ps)
      [(Int, (Term, Term))] -> TCMT IO [(Int, (Term, Term))]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
i,(Int -> Term -> Substitution
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i Term
iz Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
tm, Int -> Term -> Substitution
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i Term
io Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
tm)) | Int
i <- [Int]
vs]
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.bndry" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta2
                                  (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"bndry =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, (Term, Term))] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, (Term, Term))]
bndry
    Tele (Dom Type)
-> [Arg (Term, EqualityView)]
-> Tele (Dom Type)
-> Type
-> [(Int, (Term, Term))]
-> TCMT IO (Type, Int)
withFunctionType Tele (Dom Type)
delta1 [Arg (Term, EqualityView)]
vtys Tele (Dom Type)
delta2 Type
b [(Int, (Term, Term))]
bndry
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.type" 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
"with-function type:", 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
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
withFunType ]
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.type" Int
50 (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
"with-function type:", 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
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
withFunType ]

  Term
call_in_parent <- do
    (TelV Tele (Dom Type)
tel Type
_,Boundary
bs) <- Int -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) Type
withFunType
    Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Substitution
Substitution' (SubstArg Term)
argsS Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` QName -> Elims -> Term
Def QName
aux (Tele (Dom Type) -> Boundary -> Elims
forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
tel Boundary
bs)

  [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
$ Tele (Dom Type) -> 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) -> m a -> m a
addContext Tele (Dom Type)
delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with function call" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
call_in_parent

  -- Andreas, 2013-10-21
  -- Check generated type directly in internal syntax.
  List1 (Clause' LHS) -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange List1 (Clause' LHS)
cs (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
NoHighlighting (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$   -- To avoid flicker.
    Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Type -> Call
CheckWithFunctionType Type
withFunType) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    -- 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.
    TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM ()
forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
withFunType

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

  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.top" Int
20 [Char]
"created with display form"

  case Open DisplayForm -> DisplayForm
forall (t :: * -> *) a. Decoration t => t a -> a
dget Open DisplayForm
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, Semigroup (m Doc), 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
        ]
  QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
    Defn
fun  <- TCM Defn
forall (m :: * -> *). HasOptions m => m Defn
emptyFunction
    Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$
      (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
aux Type
withFunType Language
lang Defn
fun)
        { defDisplay = [df] }
  -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

  [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
sep
    [ TCMT IO Doc
"added with function" 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
aux) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of type"
    , 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
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
withFunType
    , 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
<+> (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope)
    ]
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" 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
vcat
    [ 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
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"raw with func. type = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
withFunType
    ]


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

  -- #4833: inherit abstract mode from parent
  IsAbstract
abstr <- Definition -> IsAbstract
defAbstract (Definition -> IsAbstract)
-> TCMT IO Definition -> TCMT IO IsAbstract
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f)

  -- Check the with function
  let info :: DefInfo
info = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
Info.mkDefInfo (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
aux) Fixity'
noFixity' Access
PublicAccess IsAbstract
abstr (List1 (Clause' LHS) -> Range
forall a. HasRange a => a -> Range
getRange List1 (Clause' LHS)
cs)
  ArgInfo
ai <- Definition -> ArgInfo
defArgInfo (Definition -> ArgInfo) -> TCMT IO Definition -> TCMT IO ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe (Substitution, Map Name LetBinding)
-> [Clause' LHS]
-> TCM ()
checkFunDefS Type
withFunType ArgInfo
ai Maybe ExtLamInfo
forall a. Maybe a
Nothing (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f) DefInfo
info QName
aux ((Substitution, Map Name LetBinding)
-> Maybe (Substitution, Map Name LetBinding)
forall a. a -> Maybe a
Just (Substitution
withSub, Map Name LetBinding
lets)) ([Clause' LHS] -> TCM ()) -> [Clause' LHS] -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 (Clause' LHS) -> [Item (List1 (Clause' LHS))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Clause' LHS)
cs
  Maybe Term -> TCMT IO (Maybe Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCMT IO (Maybe Term))
-> Maybe Term -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term
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
ds) TCM a
ret = do
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
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
  Maybe Declaration -> TCM a
loop Maybe Declaration
ds
  where
    loop :: Maybe Declaration -> TCM a
loop = \case
      Maybe Declaration
Nothing -> TCM a
ret
      -- [A.ScopedDecl scope ds] -> withScope_ scope $ loop ds  -- IMPOSSIBLE
      Just (A.Section Range
_ Erased
e ModuleName
m GeneralizeTelescope
tel [Declaration]
ds) -> Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
forall a.
Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection Erased
e ModuleName
m GeneralizeTelescope
tel (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
          (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCheckingWhere = True }) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
            [Declaration] -> TCM ()
checkDecls [Declaration]
ds
            TCM a
ret
      Maybe Declaration
_ -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- #2897: We can't handle named where-modules in refined contexts.
    ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
Nothing = () -> m ()
forall 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
      [Term]
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 :: * -> *).
(Functor m, Applicative 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)
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Term] -> Bool
isWeakening [Term]
args) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do -- weakened contexts are fine
        [[Char]]
names <- (Dom ([Char], Type) -> [Char]) -> [Dom ([Char], Type)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char]
argNameToString ([Char] -> [Char])
-> (Dom ([Char], Type) -> [Char]) -> Dom ([Char], Type) -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char])
-> (Dom ([Char], Type) -> ([Char], Type))
-> Dom ([Char], Type)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom) ([Dom ([Char], Type)] -> [[Char]])
-> (Tele (Dom Type) -> [Dom ([Char], Type)])
-> Tele (Dom Type)
-> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (Tele (Dom Type) -> [[Char]]) -> m (Tele (Dom Type)) -> m [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                (ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (ModuleName -> m (Tele (Dom Type)))
-> m ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
        TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [Term] -> [[Char]] -> TypeError
NamedWhereModuleInRefinedContext [Term]
args [[Char]]
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
C.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)

  Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
-> TCM a
forall a.
Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
-> TCM a
checkGeneralizeTelescope (ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
m) GeneralizeTelescope
gtel (([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a)
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ [Maybe Name]
_ Tele (Dom Type)
tel' -> do
    [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) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m

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

-- | Set the current clause number.

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