{-# 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 Control.Monad

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 (runFree, IgnoreSorts(..))
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Positivity
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.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 ProjectionView
pv =
  case ProjectionView
pv of
    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

-- | 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.
  ProjectionView
pv <- Term -> m ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
  case ProjectionView
pv of
    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

data ProjEliminator = EvenLone | ButLone | NoPostfix
  deriving ProjEliminator -> ProjEliminator -> Bool
(ProjEliminator -> ProjEliminator -> Bool)
-> (ProjEliminator -> ProjEliminator -> Bool) -> Eq ProjEliminator
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProjEliminator -> ProjEliminator -> Bool
== :: ProjEliminator -> ProjEliminator -> Bool
$c/= :: ProjEliminator -> ProjEliminator -> Bool
/= :: ProjEliminator -> ProjEliminator -> Bool
Eq

-- | 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".
--
--   If the 'Bool' is 'True', a lone projection like function will be
--   turned into a lambda-abstraction, expecting the principal argument.
--   If the 'Bool' is 'False', it will be returned unaltered.
--
--   No precondition.
--   Preserves constructorForm, since it really does only something
--   on (applications of) projection-like functions.
elimView :: PureTCM m => ProjEliminator -> Term -> m Term
elimView :: forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
pe 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
  Term
v <- Term -> m Term
forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike Term
v
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.elim" Int
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"elimView (projections reduced) 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
  case ProjEliminator
pe of
    ProjEliminator
NoPostfix -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    ProjEliminator
_         -> do
      ProjectionView
pv <- Term -> m ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
      case ProjectionView
pv of
        NoProjection{}        -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
        LoneProjectionLike QName
f ArgInfo
ai
          | ProjEliminator
peProjEliminator -> ProjEliminator -> Bool
forall a. Eq a => a -> a -> Bool
==ProjEliminator
EvenLone  -> 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]
          | Bool
otherwise     -> 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
<$> ProjEliminator -> Term -> m Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
pe (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)

-- | 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 => 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"
  Definition
defn <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  let t :: Type
t = Definition -> Type
defType Definition
defn
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" 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
sep
    [ TCMT IO Doc
"Checking for projection likeness "
    , 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    ]
  if Definition -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
defn then
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  projection-like functions cannot be irrelevant"
  else case Definition -> Defn
theDef Definition
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
                 funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
ConcreteDef, funOpaque :: Defn -> IsOpaque
funOpaque = IsOpaque
TransparentDef} -> do
      [(Arg QName, Int)]
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 -> [(Arg QName, Int)]
candidateArgs [] Type
t
      [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
$ if [(Arg QName, Int)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0 then [Char]
"  no candidates found"
                                                else [Char]
"  candidates: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Arg QName, Int)] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [(Arg QName, Int)]
ps0
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Arg QName, Int)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- Andreas 2012-09-26: only consider non-recursive functions for proj.like.
        -- Issue 700: problems with recursive funs. in term.checker and reduction
        TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
recursive ([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]
"  recursive functions are not considered for projection-likeness") (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          {- else -}
          case [(Arg QName, Int)] -> Maybe (Arg QName, Int)
forall a. [a] -> Maybe a
lastMaybe (((Arg QName, Int) -> Bool)
-> [(Arg QName, Int)] -> [(Arg QName, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Clause] -> Int -> Bool
forall {t :: * -> *}. Foldable t => t Clause -> Int -> Bool
checkOccurs [Clause]
cls (Int -> Bool)
-> ((Arg QName, Int) -> Int) -> (Arg QName, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg QName, Int) -> Int
forall a b. (a, b) -> b
snd) [(Arg QName, Int)]
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 -> 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] -> 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, MonadTCM m, 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)]
tel = Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. Int -> [a] -> [a]
take Int
pIndex ([Dom ([Char], Type)] -> [Dom ([Char], Type)])
-> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (Tele (Dom Type) -> [Dom ([Char], Type)])
-> Tele (Dom Type) -> [Dom ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ TelV Type -> Tele (Dom Type)
forall a. TelV a -> Tele (Dom a)
theTel (TelV Type -> Tele (Dom Type)) -> TelV Type -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Type -> TelV Type
telView' Type
t
              Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Dom ([Char], Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type)]
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) -> Arg [Char])
-> [Dom ([Char], Type)] -> [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) -> Dom' Term [Char])
-> Dom ([Char], Type)
-> Arg [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Type) -> [Char])
-> Dom ([Char], Type) -> 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) -> [Char]
forall a b. (a, b) -> a
fst) [Dom ([Char], Type)]
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"
    Function{funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
AbstractDef} ->
      [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"
    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
      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)

    -- NOTE: If the following definition turns out to be slow, then
    -- one could perhaps reuse information computed by the termination
    -- and/or positivity checkers.
    recursive :: TCMT IO Bool
recursive = do
      Map Item Integer
occs <- QName -> TCM (Map Item Integer)
computeOccurrences QName
x
      case Item -> Map Item Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (QName -> Item
ADef QName
x) Map Item Integer
occs of
        Just Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
1 -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- recursive occurrence
        Maybe Integer
_               -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> [NamedArg (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 -> [NamedArg (Pattern' x)] -> Bool
onlyMatch Int
n [NamedArg (Pattern' x)]
ps = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (Pattern' x)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
shallowMatch (Pattern' x -> Bool)
-> (NamedArg (Pattern' x) -> Pattern' x)
-> NamedArg (Pattern' x)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' x) -> Pattern' x
forall a. NamedArg a -> a
namedArg) (Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. Int -> [a] -> [a]
take Int
1 [NamedArg (Pattern' x)]
ps1) Bool -> Bool -> Bool
&&
                     [NamedArg (Pattern' x)] -> Bool
forall {x}. [NamedArg (Pattern' x)] -> Bool
noMatches ([NamedArg (Pattern' x)]
ps0 [NamedArg (Pattern' x)]
-> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. [a] -> [a] -> [a]
++ Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. Int -> [a] -> [a]
drop Int
1 [NamedArg (Pattern' x)]
ps1)
      where
        ([NamedArg (Pattern' x)]
ps0, [NamedArg (Pattern' x)]
ps1) = Int
-> [NamedArg (Pattern' x)]
-> ([NamedArg (Pattern' x)], [NamedArg (Pattern' x)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg (Pattern' x)]
ps
        shallowMatch :: Pattern' x -> Bool
shallowMatch (ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps) = [NamedArg (Pattern' x)] -> Bool
forall {x}. [NamedArg (Pattern' x)] -> Bool
noMatches [NamedArg (Pattern' x)]
ps
        shallowMatch Pattern' x
_             = Bool
True
        noMatches :: [NamedArg (Pattern' x)] -> Bool
noMatches = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (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)
-> (NamedArg (Pattern' x) -> Pattern' x)
-> NamedArg (Pattern' x)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (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) -> (Any -> Bool) -> Any -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar Any -> IgnoreSorts -> t -> Any
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar Any
badVar IgnoreSorts
IgnoreNot t
b
      where badVar :: SingleVar Any
badVar Int
x = Bool -> Any
Any (Bool -> Any) -> Bool -> Any
forall a b. (a -> b) -> a -> b
$ 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 -> [(Arg QName, Int)]
candidateArgs [Term]
vs Type
t =
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b
          | Def QName
d Elims
es <- 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,
            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 -> Arg QName
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
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 -> [(Arg QName, Int)]
candidateRec Abs Type
b
          | Bool
otherwise          -> Abs Type -> [(Arg QName, Int)]
candidateRec Abs Type
b
        Term
_                      -> []
      where
        candidateRec :: Abs Type -> [(Arg QName, Int)]
candidateRec NoAbs{}   = []
        candidateRec (Abs [Char]
x Type
t) = [Term] -> Type -> [(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
t

-- | 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.
inferNeutral :: (PureTCM m, MonadBlock m) => Term -> m Type
inferNeutral :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Type
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
  case Term
u of
    Var Int
i Elims
es -> do
      Type
a <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
      Type -> (Elims -> Term) -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> (Elims -> Term) -> Elims -> m Type
loop Type
a (Int -> Elims -> Term
Var Int
i) Elims
es
    Def QName
f Elims
es -> do
      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. MonadDebug m => m a
nonInferable
      Type
a <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      Type -> (Elims -> Term) -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> (Elims -> Term) -> Elims -> m Type
loop Type
a (QName -> Elims -> Term
Def QName
f) Elims
es
    MetaV MetaId
x Elims
es -> do -- we assume meta instantiations to be well-typed
      Type
a <- MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
      Type -> (Elims -> Term) -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> (Elims -> Term) -> Elims -> m Type
loop Type
a (MetaId -> Elims -> Term
MetaV MetaId
x) Elims
es
    Term
_ -> m Type
forall (m :: * -> *) a. MonadDebug m => m a
nonInferable
  where
    nonInferable :: MonadDebug m => m a
    nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
nonInferable = [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 -> (Elims -> Term) -> Elims -> m Type
loop Type
t Elims -> Term
hd [] = Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    loop Type
t Elims -> Term
hd (Elim' Term
e:Elims
es) = do
      Type
t' <- case Elim' Term
e of
        Apply (Arg ArgInfo
ai Term
v) ->
          Type
-> (Dom Type -> Abs Type -> m Type) -> (Type -> m Type) -> m Type
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType Type
t (\Dom Type
_ Abs Type
b -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v) Type -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
        IApply Term
x Term
y Term
r ->
          Type
-> (Dom Type -> Abs Type -> m Type) -> (Type -> m Type) -> m Type
forall (m :: * -> *) a.
PureTCM m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPath Type
t (\Dom Type
_ Abs Type
b -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
r) Type -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
        Proj ProjOrigin
o QName
f -> do
          -- @projectTyped@ expects the type to be reduced.
          Type
t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
          m (Maybe (Dom Type, Term, Type))
-> ((Dom Type, Term, Type) -> m Type) -> m Type -> m Type
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM (Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped (Elims -> Term
hd []) Type
t ProjOrigin
o QName
f) (\(Dom Type
_,Term
_,Type
t') -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t') m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
      Type -> (Elims -> Term) -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> (Elims -> Term) -> Elims -> m Type
loop Type
t' (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term
eElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es

-- | 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
computeDefType QName
f Elims
es = do
  Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => 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 :: m Type
defaultResult = Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  -- Find a first argument to @f@.
  case Elims
es of
    Elims
_ | Definition -> Int
projectionArgs Definition
def Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 -> m Type
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.
      Type
targ <- Term -> m Type
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Type
inferNeutral (Term -> m Type) -> m Term -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProjEliminator -> Term -> m Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
      [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
"inferred 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
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.
      Type
targ <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
targ
      m Type -> m (Maybe Type) -> m Type
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (m (Maybe Type) -> m Type) -> m (Maybe Type) -> m Type
forall a b. (a -> b) -> a -> b
$ QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
targ
    Elims
_ -> m Type
defaultResult