-- | 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.Reduce (reduce)

import Agda.TypeChecking.DropArgs

import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.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 (forall a. Arg a -> Elim' a
Apply Arg Term
a 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> ProjectionView
NoProjection Term
v
  case Term
v of
    Def QName
f Elims
es -> forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f) m ProjectionView
fallback forall a b. (a -> b) -> a -> b
$ \ Projection
isP -> do
      if Projection -> Int
projIndex Projection
isP forall a. Ord a => a -> a -> Bool
<= Int
0 then m ProjectionView
fallback else do
        case Elims
es of
          []           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> ArgInfo -> ProjectionView
LoneProjectionLike QName
f forall a b. (a -> b) -> a -> b
$ Projection -> ArgInfo
projArgInfo Projection
isP
          Apply Arg Term
a : Elims
es -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__
          -- The principal argument of a projection-like cannot be the interval?
          IApply{} : Elims
_ -> 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 <- forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
  case ProjectionView
pv of
    ProjectionView{} -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceProjections forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
                            -- ordinary reduce, only different for Def's
    ProjectionView
_                -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

data ProjEliminator = EvenLone | ButLone | NoPostfix
  deriving ProjEliminator -> ProjEliminator -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProjEliminator -> ProjEliminator -> Bool
$c/= :: ProjEliminator -> ProjEliminator -> Bool
== :: ProjEliminator -> ProjEliminator -> Bool
$c== :: 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.elim" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"elimView of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  Term
v <- forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike Term
v
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.elim" Int
65 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"elimView (projections reduced) of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  case ProjEliminator
pe of
    ProjEliminator
NoPostfix -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    ProjEliminator
_         -> do
      ProjectionView
pv <- forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
      case ProjectionView
pv of
        NoProjection{}        -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
        LoneProjectionLike QName
f ArgInfo
ai
          | ProjEliminator
peforall a. Eq a => a -> a -> Bool
==ProjEliminator
EvenLone  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
"r" forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f]
          | Bool
otherwise     -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
        ProjectionView QName
f Arg Term
a Elims
es -> (forall t. Apply t => t -> Elims -> t
`applyE` (forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f forall a. a -> [a] -> [a]
: Elims
es)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
pe (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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{} -> 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 = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optProjectionLike forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
 forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
70 forall a b. (a -> b) -> a -> b
$ [Char]
"Considering " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" for projection likeness"
  Definition
defn <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  let t :: Type
t = Definition -> Type
defType Definition
defn
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"Checking for projection likeness "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  if forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
defn then
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
30 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}
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  projection-like functions cannot have absurd clauses"
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Bool
isRecordExpression forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 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} -> do
      [(Arg QName, Int)]
ps0 <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Arg QName, Int) -> TCMT IO Bool
validProj forall a b. (a -> b) -> a -> b
$ [Term] -> Type -> [(Arg QName, Int)]
candidateArgs [] Type
t
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0 then [Char]
"  no candidates found"
                                                else [Char]
"  candidates: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(Arg QName, Int)]
ps0
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0) 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
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
recursive (forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  recursive functions are not considered for projection-likeness") forall a b. (a -> b) -> a -> b
$ do
          {- else -}
          case forall a. [a] -> Maybe a
lastMaybe (forall a. (a -> Bool) -> [a] -> [a]
filter (forall {t :: * -> *}. Foldable t => t Clause -> Int -> Bool
checkOccurs [Clause]
cls forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Arg QName, Int)]
ps0) of
            Maybe (Arg QName, Int)
Nothing -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"occurs check failed"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"clauses =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map 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!
              forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.like" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
                , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                  [ TCMT IO Doc
"is projection like in argument",  forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
n, TCMT IO Doc
"for type", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg QName
d) ]
                ]
              forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
[Char] -> Int -> m ()
__CRASH_WHEN__ [Char]
"tc.proj.like.crash" Int
1000

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

              -- Andreas, 2013-10-20 build parameter dropping function
              let pIndex :: Int
pIndex = Int
n forall a. Num a => a -> a -> a
+ Int
1
                  tel :: [Dom ([Char], Type)]
tel = forall a. Int -> [a] -> [a]
take Int
pIndex forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList forall a b. (a -> b) -> a -> b
$ forall a. TelV a -> Tele (Dom a)
theTel forall a b. (a -> b) -> a -> b
$ Type -> TelView
telView' Type
t
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type)]
tel forall a. Eq a => a -> a -> Bool
== Int
pIndex) forall a. HasCallStack => a
__IMPOSSIBLE__
              let projection :: Projection
projection = Projection
                    { projProper :: Maybe QName
projProper   = 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) [Dom ([Char], Type)]
tel
                    }
              let newDef :: Defn
newDef = Defn
def
                           { funProjection :: Either ProjectionLikenessMissing Projection
funProjection     = forall a b. b -> Either a b
Right Projection
projection
                           , funClauses :: [Clause]
funClauses        = [Clause]
cls'
                           , funSplitTree :: Maybe SplitTree
funSplitTree      = Maybe SplitTree
st
                           , funCompiled :: Maybe CompiledClauses
funCompiled       = Maybe CompiledClauses
cc
                           , funInv :: FunctionInverse
funInv            = forall a. DropArgs a => Int -> a -> a
dropArgs Int
n forall a b. (a -> b) -> a -> b
$ Defn -> FunctionInverse
funInv Defn
def
                           }
              QName -> Definition -> TCM ()
addConstant QName
x forall a b. (a -> b) -> a -> b
$ Definition
defn { defPolarity :: [Polarity]
defPolarity       = forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ Definition -> [Polarity]
defPolarity Definition
defn
                                   , defArgOccurrences :: [Occurrence]
defArgOccurrences = forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ Definition -> [Occurrence]
defArgOccurrences Definition
defn
                                   , defDisplay :: [LocalDisplayForm]
defDisplay        = []
                                   , theDef :: Defn
theDef            = Defn
newDef
                                   }
    Function{funInv :: Defn -> FunctionInverse
funInv = Inverse{}} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  injective functions can't be projections"
    Function{funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
AbstractDef} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  abstract functions can't be projections"
    Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right{}} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  already projection like"
    Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
NeverProjection} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 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]
_)} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  mutual functions can't be projections"
    Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
Nothing} ->
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  mutuality check has not run yet"
    Axiom{}        -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Axiom"
    DataOrRecSig{} -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but DataOrRecSig"
    GeneralizableVar{} -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but GeneralizableVar"
    AbstractDefn{} -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but AbstractDefn"
    Constructor{}  -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Constructor"
    Datatype{}     -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Datatype"
    Primitive{}    -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but Primitive"
    PrimitiveSort{} -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"  not a function, but PrimitiveSort"
    Record{}       -> forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
30 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) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    validProj (Arg QName
d, Int
_) = forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike (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 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 forall a. Ord a => a -> a -> Bool
>= Integer
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- recursive occurrence
        Maybe Integer
_               -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    checkOccurs :: t Clause -> Int -> Bool
checkOccurs t Clause
cls Int
n = 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 =
        (forall a. Int -> [a] -> [a]
take Int
n [Int]
p forall a. Eq a => a -> a -> Bool
== [Int
0..Int
n forall a. Num a => a -> a -> a
- Int
1]) Bool -> Bool -> Bool
&&
        forall {x}. Int -> [NamedArg (Pattern' x)] -> Bool
onlyMatch Int
n NAPs
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
        forall {t}. Free t => Int -> Int -> t -> Bool
checkBody Int
m Int
n Maybe Term
b
      where
        Perm Int
_ [Int]
p = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
cl
        ps :: NAPs
ps       = Clause -> NAPs
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        = forall a. Sized a => a -> Int
size forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars NAPs
ps  -- This also counts dot patterns!


    onlyMatch :: Int -> [NamedArg (Pattern' x)] -> Bool
onlyMatch Int
n [NamedArg (Pattern' x)]
ps = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
shallowMatch forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) (forall a. Int -> [a] -> [a]
take Int
1 [NamedArg (Pattern' x)]
ps1) Bool -> Bool -> Bool
&&
                     forall {x}. [NamedArg (Pattern' x)] -> Bool
noMatches ([NamedArg (Pattern' x)]
ps0 forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop Int
1 [NamedArg (Pattern' x)]
ps1)
      where
        ([NamedArg (Pattern' x)]
ps0, [NamedArg (Pattern' x)]
ps1) = 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) = forall {x}. [NamedArg (Pattern' x)] -> Bool
noMatches [NamedArg (Pattern' x)]
ps
        shallowMatch Pattern' x
_             = Bool
True
        noMatches :: [NamedArg (Pattern' x)] -> Bool
noMatches = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall {x}. Pattern' x -> Bool
noMatch forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> Any
badVar IgnoreSorts
IgnoreNot t
b
      where badVar :: Int -> Any
badVar Int
x = Bool -> Any
Any forall a b. (a -> b) -> a -> b
$ Int
m forall a. Num a => a -> a -> a
- Int
n forall a. Ord a => a -> a -> Bool
<= Int
x Bool -> Bool -> Bool
&& Int
x 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 forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b
          | Def QName
d Elims
es <- forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a,
            Just [Arg Term]
us  <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es,
            [Term]
vs forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Term]
us -> (QName
d forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs) 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 (forall a. Sized a => a -> Int
size [Term]
vs) forall a. a -> [a] -> [a]
: [Term]
vs) Type
t