-- {-# OPTIONS_GHC -Wunused-imports #-}

-- | Dropping initial arguments (``parameters'') from a function which can be
--   easily reconstructed from its principal argument.
--
--   A function which has such parameters is called ``projection-like''.
--
--   The motivation for this optimization comes from the use of nested records.
--
--   First, let us look why proper projections need not store the parameters:
--   The type of a projection @f@ is of the form
--   @
--      f : Γ → R Γ → C
--   @
--   where @R@ is the record type and @C@ is the type of the field @f@.
--   Given a projection application
--   @
--      p pars u
--   @
--   we know that the type of the principal argument @u@ is
--   @
--      u : R pars
--   @
--   thus, the parameters @pars@ are redundant in the projection application
--   if we can always infer the type of @u@.
--   For projections, this is case, because the principal argument @u@ must be
--   neutral; otherwise, if it was a record value, we would have a redex,
--   yet Agda maintains a β-normal form.
--
--   The situation for projections can be generalized to ``projection-like''
--   functions @f@.  Conditions:
--
--     1. The type of @f@ is of the form @f : Γ → D Γ → ...@ for some
--        type constructor @D@ which can never reduce.
--
--     2. For every reduced welltyped application @f pars u ...@,
--        the type of @u@ is inferable.
--
--   This then allows @pars@ to be dropped always.
--
--   Condition 2 is approximated by a bunch of criteria, for details see function
--   'makeProjection'.
--
--   Typical projection-like functions are compositions of projections
--   which arise from nested records.
--
--   Notes:
--
--     1. This analysis could be dualized to ``constructor-like'' functions
--        whose parameters are reconstructable from the target type.
--        But such functions would need to be fully applied.
--
--     2. A more general analysis of which arguments are reconstructible
--        can be found in
--
--          Jason C. Reed, Redundancy elimination for LF
--          LFTMP 2004.

module Agda.TypeChecking.ProjectionLike where

import qualified Data.Map as Map
-- import Data.Monoid (Any(..), getAny)

import Agda.Interaction.Options

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free (anyFreeVar)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Positivity.OccurrenceAnalysis qualified as Occ
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce (reduce, abortIfBlocked)
import Agda.TypeChecking.Telescope

import Agda.TypeChecking.DropArgs

import Agda.Utils.CallStack (HasCallStack)
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | View for a @Def f (Apply a : es)@ where @isRelevantProjection f@.
--   Used for projection-like @f@s.
data ProjectionView
  = ProjectionView
    { ProjectionView -> QName
projViewProj  :: QName
    , ProjectionView -> Arg Term
projViewSelf  :: Arg Term
    , ProjectionView -> Elims
projViewSpine :: Elims
    }
    -- ^ A projection or projection-like function, applied to its
    --   principal argument
  | LoneProjectionLike QName ArgInfo
    -- ^ Just a lone projection-like function, missing its principal
    --   argument (from which we could infer the parameters).
  | NoProjection Term
    -- ^ Not a projection or projection-like thing.

-- | Semantics of 'ProjectionView'.
unProjView :: ProjectionView -> Term
unProjView :: ProjectionView -> Term
unProjView = \case
    ProjectionView QName
f Arg Term
a Elims
es   -> QName -> Elims -> Term
Def QName
f (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
a Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es)
    LoneProjectionLike QName
f ArgInfo
ai -> QName -> Elims -> Term
Def QName
f []
    NoProjection Term
v          -> Term
v

-- | Top-level 'ProjectionView' (no reduction).
{-# SPECIALIZE projView :: Term -> TCM ProjectionView #-}
projView :: HasConstInfo m => Term -> m ProjectionView
projView :: forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v = do
  let fallback :: m ProjectionView
fallback = ProjectionView -> m ProjectionView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ Term -> ProjectionView
NoProjection Term
v
  case Term
v of
    Def QName
f Elims
es -> m (Maybe Projection)
-> m ProjectionView
-> (Projection -> m ProjectionView)
-> m ProjectionView
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) m ProjectionView
fallback ((Projection -> m ProjectionView) -> m ProjectionView)
-> (Projection -> m ProjectionView) -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ \ Projection
isP -> do
      if Projection -> Int
projIndex Projection
isP Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then m ProjectionView
fallback else do
        case Elims
es of
          []           -> ProjectionView -> m ProjectionView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ QName -> ArgInfo -> ProjectionView
LoneProjectionLike QName
f (ArgInfo -> ProjectionView) -> ArgInfo -> ProjectionView
forall a b. (a -> b) -> a -> b
$ Projection -> ArgInfo
projArgInfo Projection
isP
          Apply Arg Term
a : Elims
es -> ProjectionView -> m ProjectionView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ QName -> Arg Term -> Elims -> ProjectionView
ProjectionView QName
f Arg Term
a Elims
es
          -- Since a projection is a function, it cannot be projected itself.
          Proj{}  : Elims
_  -> m ProjectionView
forall a. HasCallStack => a
__IMPOSSIBLE__
          -- The principal argument of a projection-like cannot be the interval?
          IApply{} : Elims
_ -> m ProjectionView
forall a. HasCallStack => a
__IMPOSSIBLE__

    Term
_ -> m ProjectionView
fallback

{-# SPECIALIZE reduceProjectionLike :: Term -> TCM Term #-}
-- | Reduce away top-level projection like functions.
--   (Also reduces projections, but they should not be there,
--   since Internal is in lambda- and projection-beta-normal form.)
--
reduceProjectionLike :: PureTCM m => Term -> m Term
reduceProjectionLike :: forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike Term
v = do
  -- Andreas, 2013-11-01 make sure we do not reduce a constructor
  -- because that could be folded back into a literal by reduce.
  Term -> m ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v m ProjectionView -> (ProjectionView -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ProjectionView{} -> m Term -> m Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceProjections (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
                            -- ordinary reduce, only different for Def's
    ProjectionView
_                -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | How to treat lone projection-like functions
--   (i.e. those that miss their principal argument) in 'elimView'.
data LoneProjectionLikeToLambda
  = LoneProjectionLikeToLambda
      -- ^ Turn lone projection-like functions into lambdas.
  | KeepLoneProjectionLike
      -- ^ Leave lone projection-like functions as they are.
  deriving LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool
(LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool)
-> (LoneProjectionLikeToLambda
    -> LoneProjectionLikeToLambda -> Bool)
-> Eq LoneProjectionLikeToLambda
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool
== :: LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool
$c/= :: LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool
/= :: LoneProjectionLikeToLambda -> LoneProjectionLikeToLambda -> Bool
Eq

{-# SPECIALIZE elimView :: LoneProjectionLikeToLambda -> Term -> TCM Term #-}
-- | Turn prefix projection-like function application into postfix ones.
--   This does just one layer, such that the top spine contains
--   the projection-like functions as projections.
--   Used in 'compareElims' in @TypeChecking.Conversion@
--   and in "Agda.TypeChecking.CheckInternal".
--
--   With 'LoneProjectionLikeToLambda', a lone projection like function will be
--   turned into a lambda-abstraction, expecting the principal argument.
--   If the 'KeepLoneProjectionLike', it will be returned unaltered.
--
--   No precondition.
--   Preserves constructorForm, since it really does only something
--   on (applications of) projection-like functions.
elimView :: PureTCM m => LoneProjectionLikeToLambda -> Term -> m Term
elimView :: forall (m :: * -> *).
PureTCM m =>
LoneProjectionLikeToLambda -> Term -> m Term
elimView LoneProjectionLikeToLambda
loneProjectionLikeToLambda Term
v = do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.elim" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"elimView of " 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
  v <- Term -> m Term
forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike Term
v
  reportSDoc "tc.conv.elim" 65 $
    "elimView (projections reduced) of " <+> prettyTCM v
  projView v >>= \case
    LoneProjectionLike QName
f ArgInfo
ai -> case LoneProjectionLikeToLambda
loneProjectionLikeToLambda of
      LoneProjectionLikeToLambda
LoneProjectionLikeToLambda -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
"r" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f]
      LoneProjectionLikeToLambda
KeepLoneProjectionLike -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    ProjectionView QName
f Arg Term
a Elims
es -> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` (ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es)) (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoneProjectionLikeToLambda -> Term -> m Term
forall (m :: * -> *).
PureTCM m =>
LoneProjectionLikeToLambda -> Term -> m Term
elimView LoneProjectionLikeToLambda
loneProjectionLikeToLambda (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
    NoProjection{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

{-# SPECIALIZE eligibleForProjectionLike :: QName -> TCM Bool #-}
-- | Which @Def@types are eligible for the principle argument
--   of a projection-like function?
eligibleForProjectionLike :: (HasConstInfo m) => QName -> m Bool
eligibleForProjectionLike :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike QName
d = Defn -> Bool
eligible (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> m Definition -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
  where
  eligible :: Defn -> Bool
eligible = \case
    Datatype{} -> Bool
True
    Record{}   -> Bool
True
    Axiom{}    -> Bool
True
    DataOrRecSig{}     -> Bool
True
    GeneralizableVar{} -> Bool
False
    Function{}    -> Bool
False
    Primitive{}   -> Bool
False
    PrimitiveSort{} -> Bool
False
    Constructor{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    AbstractDefn Defn
d -> Defn -> Bool
eligible Defn
d
      -- Andreas, 2017-08-14, issue #2682:
      -- Abstract records still export the projections.
      -- Andreas, 2016-10-11 AIM XXIV
      -- Projection-like at abstract types violates the parameter reconstructibility property.
      -- See test/Fail/AbstractTypeProjectionLike.

-- | Turn a definition into a projection if it looks like a projection.
--
-- Conditions for projection-likeness of @f@:
--
--   1. The type of @f@ must be of the shape @Γ → D Γ → C@ for @D@
--      a name (@Def@) which is 'eligibleForProjectionLike':
--      @data@ / @record@ / @postulate@.
--
--   2. The application of f should only get stuck if the principal argument
--      is inferable (neutral).  Thus:
--
--      a. @f@ cannot have absurd clauses (which are stuck even if the principal
--         argument is a constructor).
--
--      b. @f@ cannot be abstract as it does not reduce outside abstract blocks
--         (always stuck).
--
--      c. @f@ cannot match on other arguments than the principal argument.
--
--      d. @f@ cannot match deeply.
--
--      e. @f@s body may not mention the parameters.
--
--      f. A rhs of @f@ cannot be a record expression, since this will be
--         translated to copatterns by recordExpressionsToCopatterns.
--         Thus, an application of @f@ waiting for a projection
--         can be stuck even when the principal argument is a constructor.
--
--      g. @f@ cannot be an irrelevant definition (Andreas, 2022-03-07, #5809),
--         as those are not reduced.
--
-- For internal reasons:
--
--   3. @f@ cannot be constructor headed
--
--   4. @f@ cannot be recursive, since we have not implemented a function
--      which goes through the bodies of the @f@ and the mutually recursive
--      functions and drops the parameters from all applications of @f@.
--
-- Examples for these reasons: see test/Succeed/NotProjectionLike.agda

makeProjection :: QName -> TCM ()
makeProjection :: QName -> TCM ()
makeProjection QName
x = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optProjectionLike (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
$ do
 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
$ do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
70 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Considering " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for projection likeness"
  defn <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
  let t = Definition -> Type'' Term Term
defType Definition
defn
  reportSDoc "tc.proj.like" 20 $ sep
    [ "Checking for projection likeness "
    , prettyTCM x <+> " : " <+> prettyTCM t
    ]
  if isIrrelevant defn then
    reportSDoc "tc.proj.like" 30 $ "  projection-like functions cannot be irrelevant"
  else case theDef defn of
    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls}
      | (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  projection-like functions cannot have absurd clauses"
      | (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> (Term -> Bool) -> Maybe Term -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Bool
isRecordExpression (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  projection-like functions cannot have record rhss"
    -- Constructor-headed functions can't be projection-like (at the moment). The reason
    -- for this is that invoking constructor-headedness will circumvent the inference of
    -- the dropped arguments.
    -- Nor can abstract definitions be projection-like since they won't reduce
    -- outside the abstract block.
    def :: Defn
def@Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
MaybeProjection, funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls,
                 funSplitTree :: Defn -> Maybe SplitTree
funSplitTree = Maybe SplitTree
st0, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc0, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
NotInjective,
                 funMutual :: Defn -> Maybe [QName]
funMutual = Just [], -- Andreas, 2012-09-28: only consider non-mutual funs
                 funOpaque :: Defn -> IsOpaque
funOpaque = IsOpaque
TransparentDef} | Bool -> Bool
not (Defn
def Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funAbstract) -> do
      ps0 <- ((Arg QName, Int) -> TCMT IO Bool)
-> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Arg QName, Int) -> TCMT IO Bool
validProj ([(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)])
-> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
forall a b. (a -> b) -> a -> b
$ [Term] -> Type'' Term Term -> [(Arg QName, Int)]
candidateArgs [] Type'' Term Term
t
      reportSLn "tc.proj.like" 30 $ if null ps0 then "  no candidates found"
                                                else "  candidates: " ++ prettyShow ps0
      unless (null ps0) $ do
        -- Andreas 2012-09-26: only consider non-recursive functions for proj.like.
        -- Issue 700: problems with recursive funs. in term.checker and reduction
        ifM recursive (reportSLn "tc.proj.like" 30 $ "  recursive functions are not considered for projection-likeness") $ do
          {- else -}
          case lastMaybe (filter (checkOccurs cls . snd) ps0) of
            Maybe (Arg QName, Int)
Nothing -> [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
"occurs check failed"
              , 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
"clauses =" 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 ((Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Clause]
cls) ]
            Just (Arg QName
d, Int
n) -> do
              -- Yes, we are projection-like!
              [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" 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
                [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
                , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                  [ TCMT IO Doc
"is projection like in argument",  Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
n, TCMT IO Doc
"for type", QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
d) ]
                ]
              [Char] -> Int -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadDebug m) =>
[Char] -> Int -> m ()
__CRASH_WHEN__ [Char]
"tc.proj.like.crash" Int
1000

              let cls' :: [Clause]
cls' = (Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Clause -> Clause
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n) [Clause]
cls
                  cc :: Maybe CompiledClauses
cc   = Int -> Maybe CompiledClauses -> Maybe CompiledClauses
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n Maybe CompiledClauses
cc0
                  st :: Maybe SplitTree
st   = Int -> Maybe SplitTree -> Maybe SplitTree
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n Maybe SplitTree
st0
              [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
60 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
                [ [Char]
"  rewrote clauses to"
                , [Char]
"    " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> [Char]
forall a. Show a => a -> [Char]
show Maybe CompiledClauses
cc
                ]

              -- Andreas, 2013-10-20 build parameter dropping function
              let pIndex :: Int
pIndex = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                  tel :: [Dom ([Char], Type'' Term Term)]
tel = Int
-> [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
forall a. Int -> [a] -> [a]
take Int
pIndex ([Dom ([Char], Type'' Term Term)]
 -> [Dom ([Char], Type'' Term Term)])
-> [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (Tele (Dom (Type'' Term Term)) -> [Dom ([Char], Type'' Term Term)])
-> Tele (Dom (Type'' Term Term))
-> [Dom ([Char], Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ TelV (Type'' Term Term) -> Tele (Dom (Type'' Term Term))
forall a. TelV a -> Tele (Dom a)
theTel (TelV (Type'' Term Term) -> Tele (Dom (Type'' Term Term)))
-> TelV (Type'' Term Term) -> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TelV (Type'' Term Term)
telView' Type'' Term Term
t
              Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([Dom ([Char], Type'' Term Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type'' Term Term)]
tel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
pIndex) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
              let projection :: Projection
projection = Projection
                    { projProper :: Maybe QName
projProper   = Maybe QName
forall a. Maybe a
Nothing
                    , projOrig :: QName
projOrig     = QName
x
                    , projFromType :: Arg QName
projFromType = Arg QName
d
                    , projIndex :: Int
projIndex    = Int
pIndex
                    , projLams :: ProjLams
projLams     = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type'' Term Term) -> Arg [Char])
-> [Dom ([Char], Type'' Term Term)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term [Char] -> Arg [Char])
-> (Dom ([Char], Type'' Term Term) -> Dom' Term [Char])
-> Dom ([Char], Type'' Term Term)
-> Arg [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Type'' Term Term) -> [Char])
-> Dom ([Char], Type'' Term Term) -> Dom' Term [Char]
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type'' Term Term) -> [Char]
forall a b. (a, b) -> a
fst) [Dom ([Char], Type'' Term Term)]
tel
                    }
              let newDef :: Defn
newDef = Defn
def
                           { funProjection     = Right projection
                           , funClauses        = cls'
                           , funSplitTree      = st
                           , funCompiled       = cc
                           , funInv            = dropArgs n $ funInv def
                           }
              QName -> Definition -> TCM ()
addConstant QName
x (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ Definition
defn { defPolarity       = drop n $ defPolarity defn
                                   , defArgOccurrences = drop n $ defArgOccurrences defn
                                   , defDisplay        = []
                                   , theDef            = newDef
                                   }
    Function{funInv :: Defn -> FunctionInverse
funInv = Inverse{}} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  injective functions can't be projections"
    d :: Defn
d@Function{} | Defn
d Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funAbstract ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  abstract functions can't be projections"
    Function{funOpaque :: Defn -> IsOpaque
funOpaque = OpaqueDef OpaqueId
_} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  opaque functions can't be projections"
    Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right{}} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  already projection like"
    Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
NeverProjection} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  the user has asked for it not to be projection-like"
    Function{funMutual :: Defn -> Maybe [QName]
funMutual = Just (QName
_:[QName]
_)} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  mutual functions can't be projections"
    Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
Nothing} ->
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  mutuality check has not run yet"
    Function{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- match is complete, but GHC does not see this (because of d^.funAbstract)
    Axiom{}        -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Axiom"
    DataOrRecSig{} -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but DataOrRecSig"
    GeneralizableVar{} -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but GeneralizableVar"
    AbstractDefn{} -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but AbstractDefn"
    Constructor{}  -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Constructor"
    Datatype{}     -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Datatype"
    Primitive{}    -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Primitive"
    PrimitiveSort{} -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but PrimitiveSort"
    Record{}       -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Record"
  where
    -- If the user wrote a record expression as rhs,
    -- the recordExpressionsToCopatterns translation will turn this into copatterns,
    -- violating the conditions of projection-likeness.
    -- Andreas, 2019-07-11, issue #3843.
    isRecordExpression :: Term -> Bool
    isRecordExpression :: Term -> Bool
isRecordExpression = \case
      Con ConHead
_ ConOrigin
ConORec Elims
_ -> Bool
True
      Con ConHead
_ ConOrigin
ConORecWhere Elims
_ -> Bool
True
      Term
_ -> Bool
False
    -- @validProj (d,n)@ checks whether the head @d@ of the type of the
    -- @n@th argument is injective in all args (i.d. being name of data/record/axiom).
    validProj :: (Arg QName, Int) -> TCM Bool
    validProj :: (Arg QName, Int) -> TCMT IO Bool
validProj (Arg QName
_, Int
0) = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    validProj (Arg QName
d, Int
_) = QName -> TCMT IO Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
d)

    recursive :: TCMT IO Bool
recursive = QName -> TCM (Maybe [QName])
getMutual QName
x TCM (Maybe [QName])
-> (Maybe [QName] -> TCMT IO Bool) -> TCMT IO Bool
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
      Just []     -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      Just (QName
_:[]) -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      Just [QName]
_      -> TCMT IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ -- makeProjection only gets called on singleton mutual blocks
      Maybe [QName]
_           -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

    checkOccurs :: t Clause -> Int -> Bool
checkOccurs t Clause
cls Int
n = (Clause -> Bool) -> t Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Clause -> Bool
nonOccur Int
n) t Clause
cls

    nonOccur :: Int -> Clause -> Bool
nonOccur Int
n Clause
cl =
        (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n [Int]
p [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int
0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) Bool -> Bool -> Bool
&&
        Int -> [NamedArg DeBruijnPattern] -> Bool
forall {x}. Int -> [Arg (Named_ (Pattern' x))] -> Bool
onlyMatch Int
n [NamedArg DeBruijnPattern]
ps Bool -> Bool -> Bool
&&  -- projection-like functions are only allowed to match on the eliminatee
                          -- otherwise we may end up projecting from constructor applications, in
                          -- which case we can't reconstruct the dropped parameters
        Int -> Int -> Maybe Term -> Bool
forall {t}. Free t => Int -> Int -> t -> Bool
checkBody Int
m Int
n Maybe Term
b
      where
        Perm Int
_ [Int]
p = 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
$ Clause -> Maybe Permutation
clausePerm Clause
cl
        ps :: [NamedArg DeBruijnPattern]
ps       = Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
        b :: Maybe Term
b        = Clause -> Maybe Term
compiledClauseBody Clause
cl  -- Renumbers variables to match order in patterns
                                          -- and includes dot patterns as variables.
        m :: Int
m        = [Arg (Either DBPatVar Term)] -> Int
forall a. Sized a => a -> Int
size ([Arg (Either DBPatVar Term)] -> Int)
-> [Arg (Either DBPatVar Term)] -> Int
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> [Arg (Either DBPatVar Term)])
-> [NamedArg DeBruijnPattern] -> [Arg (Either DBPatVar Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NamedArg DeBruijnPattern
-> [Arg (Either (PatternVarOut (NamedArg DeBruijnPattern)) Term)]
NamedArg DeBruijnPattern -> [Arg (Either DBPatVar Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg DeBruijnPattern]
ps  -- This also counts dot patterns!


    onlyMatch :: Int -> [Arg (Named_ (Pattern' x))] -> Bool
onlyMatch Int
n [Arg (Named_ (Pattern' x))]
ps = (Arg (Named_ (Pattern' x)) -> Bool)
-> [Arg (Named_ (Pattern' x))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
shallowMatch (Pattern' x -> Bool)
-> (Arg (Named_ (Pattern' x)) -> Pattern' x)
-> Arg (Named_ (Pattern' x))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ (Pattern' x)) -> Pattern' x
forall a. NamedArg a -> a
namedArg) (Int -> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
forall a. Int -> [a] -> [a]
take Int
1 [Arg (Named_ (Pattern' x))]
ps1) Bool -> Bool -> Bool
&&
                     [Arg (Named_ (Pattern' x))] -> Bool
forall {x}. [Arg (Named_ (Pattern' x))] -> Bool
noMatches ([Arg (Named_ (Pattern' x))]
ps0 [Arg (Named_ (Pattern' x))]
-> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
forall a. [a] -> [a] -> [a]
++ Int -> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
forall a. Int -> [a] -> [a]
drop Int
1 [Arg (Named_ (Pattern' x))]
ps1)
      where
        ([Arg (Named_ (Pattern' x))]
ps0, [Arg (Named_ (Pattern' x))]
ps1) = Int
-> [Arg (Named_ (Pattern' x))]
-> ([Arg (Named_ (Pattern' x))], [Arg (Named_ (Pattern' x))])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Named_ (Pattern' x))]
ps
        shallowMatch :: Pattern' x -> Bool
shallowMatch (ConP ConHead
_ ConPatternInfo
_ [Arg (Named_ (Pattern' x))]
ps) = [Arg (Named_ (Pattern' x))] -> Bool
forall {x}. [Arg (Named_ (Pattern' x))] -> Bool
noMatches [Arg (Named_ (Pattern' x))]
ps
        shallowMatch Pattern' x
_             = Bool
True
        noMatches :: [Arg (Named_ (Pattern' x))] -> Bool
noMatches = (Arg (Named_ (Pattern' x)) -> Bool)
-> [Arg (Named_ (Pattern' x))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
forall {x}. Pattern' x -> Bool
noMatch (Pattern' x -> Bool)
-> (Arg (Named_ (Pattern' x)) -> Pattern' x)
-> Arg (Named_ (Pattern' x))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ (Pattern' x)) -> Pattern' x
forall a. NamedArg a -> a
namedArg)
        noMatch :: Pattern' x -> Bool
noMatch ConP{} = Bool
False
        noMatch DefP{} = Bool
False
        noMatch LitP{} = Bool
False
        noMatch ProjP{}= Bool
False
        noMatch VarP{} = Bool
True
        noMatch DotP{} = Bool
True
        noMatch IApplyP{} = Bool
True

    -- Make sure non of the parameters occurs in the body of the function.
    checkBody :: Int -> Int -> t -> Bool
checkBody Int
m Int
n t
b = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> t -> Bool
forall t. Free t => (Int -> Bool) -> t -> Bool
anyFreeVar Int -> Bool
badVar t
b
      where badVar :: Int -> Bool
badVar Int
x = Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m

    -- @candidateArgs [var 0,...,var(n-1)] t@ adds @(n,d)@ to the output,
    -- if @t@ is a function-type with domain @t 0 .. (n-1)@
    -- (the domain of @t@ is the type of the arg @n@).
    --
    -- This means that from the type of arg @n@ all previous arguments
    -- can be computed by a simple matching.
    -- (Provided the @d@ is data/record/postulate, checked in @validProj@).
    --
    -- E.g. f : {x : _}(y : _){z : _} -> D x y z -> ...
    -- will return (D,3) as a candidate (amongst maybe others).
    --
    candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
    candidateArgs :: [Term] -> Type'' Term Term -> [(Arg QName, Int)]
candidateArgs [Term]
vs Type'' Term Term
t =
      case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t of
        Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
          | Def QName
d Elims
es <- Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term) -> Type'' Term Term -> Term
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
a,
            Just [Arg Term]
us  <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es,
            [Term]
vs [Term] -> [Term] -> Bool
forall a. Eq a => a -> a -> Bool
== (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]
us -> (QName
d QName -> Arg (Type'' Term Term) -> Arg QName
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (Type'' Term Term) -> Arg (Type'' Term Term)
forall t a. Dom' t a -> Arg a
argFromDom Dom (Type'' Term Term)
a, [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs) (Arg QName, Int) -> [(Arg QName, Int)] -> [(Arg QName, Int)]
forall a. a -> [a] -> [a]
: Abs (Type'' Term Term) -> [(Arg QName, Int)]
candidateRec Abs (Type'' Term Term)
b
          | Bool
otherwise          -> Abs (Type'' Term Term) -> [(Arg QName, Int)]
candidateRec Abs (Type'' Term Term)
b
        Term
_                      -> []
      where
        candidateRec :: Abs (Type'' Term Term) -> [(Arg QName, Int)]
candidateRec NoAbs{}   = []
        candidateRec (Abs [Char]
x Type'' Term Term
t) = [Term] -> Type'' Term Term -> [(Arg QName, Int)]
candidateArgs (Int -> Term
var ([Term] -> Int
forall a. Sized a => a -> Int
size [Term]
vs) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs) Type'' Term Term
t

{-# SPECIALIZE inferNeutral :: Term -> TCM Type #-}
-- | Infer type of a neutral term.
--   See also @infer@ in @Agda.TypeChecking.CheckInternal@, which has a very similar
--   logic but also type checks all arguments.
--
--   Precondition: the term is not a projection-like function in prefix ('Def') form.
inferNeutral :: (PureTCM m, MonadBlock m) => Term -> m Type
inferNeutral :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (Type'' Term Term)
inferNeutral Term
u = do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.infer" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferNeutral" 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
u
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.infer" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferNeutral (rawer)" 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
u
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.infer" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"in Context" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Tele (Dom (Type'' Term Term)) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Tele (Dom (Type'' Term Term)) -> m Doc
prettyTCM (Tele (Dom (Type'' Term Term)) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom (Type'' Term Term))) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom (Type'' Term Term)))
getContextTelescope)
  case Term
u of
    Var Int
i Elims
es -> do
      a <- Int -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
i
      loop a (Var i) es
    Def QName
f Elims
es -> do
      -- f is not a lone projection-like function, see precondition.
      m (Maybe Projection) -> (Projection -> m ()) -> m ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) ((Projection -> m ()) -> m ()) -> (Projection -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Projection
_ -> m ()
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
      a <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> m Definition -> m (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      loop a (Def f) es
    MetaV MetaId
x Elims
es -> do -- we assume meta instantiations to be well-typed
      a <- MetaId -> m (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
metaType MetaId
x
      loop a (MetaV x) es
    Con{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Lit{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Lam{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Pi{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Sort{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Level{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    Dummy{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
    DontCare{} -> m (Type'' Term Term)
forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible
  where
    impossible :: (HasCallStack, MonadDebug m) => m a
    impossible :: forall (m :: * -> *) a. (HasCallStack, MonadDebug m) => m a
impossible = [Char] -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ ([Char] -> m a) -> [Char] -> m a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
      [ [Char]
"inferNeutral: non-inferable term:"
      , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Term
u
      ]
    loop :: (PureTCM m, MonadBlock m) => Type -> (Elims -> Term) -> Elims -> m Type
    loop :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type'' Term Term
-> (Elims -> Term) -> Elims -> m (Type'' Term Term)
loop Type'' Term Term
t Elims -> Term
hd [] = Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
t
    loop Type'' Term Term
t Elims -> Term
hd (Elim' Term
e:Elims
es) = do
      t' <- case Elim' Term
e of
        Apply (Arg ArgInfo
ai Term
v) ->
          Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term) -> m (Type'' Term Term))
-> (Blocked (Type'' Term Term) -> m (Type'' Term Term))
-> m (Type'' Term Term)
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiTypeB Type'' Term Term
t (\Dom (Type'' Term Term)
_ Abs (Type'' Term Term)
b -> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> m (Type'' Term Term))
-> Type'' Term Term -> m (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term)
b Abs (Type'' Term Term)
-> SubstArg (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg (Type'' Term Term)
v)
            (Blocker -> m (Type'' Term Term)
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> m (Type'' Term Term))
-> (Blocked (Type'' Term Term) -> Blocker)
-> Blocked (Type'' Term Term)
-> m (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked (Type'' Term Term) -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker) -- Andreas, 2025-12-06, issue #8263 not __IMPOSSIBLE__
        IApply Term
x Term
y Term
r ->
          Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term) -> m (Type'' Term Term))
-> (Blocked (Type'' Term Term) -> m (Type'' Term Term))
-> m (Type'' Term Term)
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPathB Type'' Term Term
t (\Dom (Type'' Term Term)
_ Abs (Type'' Term Term)
b -> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> m (Type'' Term Term))
-> Type'' Term Term -> m (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term)
b Abs (Type'' Term Term)
-> SubstArg (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg (Type'' Term Term)
r)
            (Blocker -> m (Type'' Term Term)
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> m (Type'' Term Term))
-> (Blocked (Type'' Term Term) -> Blocker)
-> Blocked (Type'' Term Term)
-> m (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked (Type'' Term Term) -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker) -- Andreas, 2025-12-06, issue #8263 this might not be __IMPOSSIBLE__ either, play it safe!
        Proj ProjOrigin
o QName
f -> do
          -- @projectTyped@ expects the type to be reduced.
          t <- Type'' Term Term -> m (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
t
          ifJustM (projectTyped (hd []) t o f) (\(Dom (Type'' Term Term)
_,Term
_,Type'' Term Term
t') -> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
t') __IMPOSSIBLE__
      loop t' (hd . (e:)) es

{-# SPECIALIZE computeDefType :: QName -> Elims -> TCM Type #-}
-- | Compute the head type of a Def application. For projection-like functions
--   this requires inferring the type of the principal argument.
computeDefType :: (PureTCM m, MonadBlock m) => QName -> Elims -> m Type
computeDefType :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Elims -> m (Type'' Term Term)
computeDefType QName
f Elims
es = do
  def <- QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
  -- To compute the type @a@ of a projection-like @f@,
  -- we have to infer the type of its first argument.
  let defaultResult = Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> m (Type'' Term Term))
-> Type'' Term Term -> m (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Definition -> Type'' Term Term
defType Definition
def
  -- Find a first argument to @f@.
  case es of
    Elims
_ | Definition -> Int
projectionArgs Definition
def Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 -> m (Type'' Term Term)
defaultResult
    (Apply Arg Term
arg : Elims
_) -> do
      -- Infer its type.
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.infer" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"inferring type of internal arg: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
arg
      -- Jesper, 2023-02-06: infer crashes on non-inferable terms,
      -- e.g. applications of projection-like functions. Hence we bring them
      -- into postfix form.
      targ <- Term -> m (Type'' Term Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (Type'' Term Term)
inferNeutral (Term -> m (Type'' Term Term)) -> m Term -> m (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LoneProjectionLikeToLambda -> Term -> m Term
forall (m :: * -> *).
PureTCM m =>
LoneProjectionLikeToLambda -> Term -> m Term
elimView LoneProjectionLikeToLambda
LoneProjectionLikeToLambda (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
      reportSDoc "tc.infer" 30 $
        "inferred type: " <+> prettyTCM targ
      -- getDefType wants the argument type reduced.
      -- Andreas, 2016-02-09, Issue 1825: The type of arg might be
      -- a meta-variable, e.g. in interactive development.
      -- In this case, we postpone.
      targ <- abortIfBlocked targ
      fromMaybeM __IMPOSSIBLE__ $ getDefType f targ
    Elims
_ -> m (Type'' Term Term)
defaultResult