-- | 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 (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 :: Term -> m ProjectionView
projView Term
v = do
  let fallback :: m ProjectionView
fallback = ProjectionView -> m ProjectionView
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 (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 (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 :: 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 (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
/= :: 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 :: ProjEliminator -> Term -> m Term
elimView ProjEliminator
pe Term
v = do
  VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.elim" Int
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"elimView of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  Term
v <- Term -> m Term
forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike Term
v
  VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.elim" Int
40 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"elimView (projections reduced) of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  case ProjEliminator
pe of
    ProjEliminator
NoPostfix -> Term -> m Term
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 (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 (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
$ VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"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 (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 :: 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
  VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
70 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Considering " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" 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
  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.proj.like" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCM Doc
"Checking for projection likeness "
    , QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  if Definition -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
defn then
    VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.proj.like" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM 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 ->
        VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  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 ->
        VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  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 -> Maybe Projection
funProjection = Maybe Projection
Nothing, 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 <- ((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
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ if [(Arg QName, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0 then VerboseKey
"  no candidates found"
                                                else VerboseKey
"  candidates: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(Arg QName, Int)] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [(Arg QName, Int)]
ps0
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Arg QName, Int)] -> 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 (VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  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 -> VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.proj.like" Int
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCM Doc
"occurs check failed"
              , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"clauses =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCM 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!
              VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.proj.like" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
                , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                  [ TCM Doc
"is projection like in argument",  Int -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
n, TCM Doc
"for type", QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
d) ]
                ]
              VerboseKey -> Int -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> Int -> m ()
__CRASH_WHEN__ VerboseKey
"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
              VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> VerboseKey
unlines
                [ VerboseKey
"  rewrote clauses to"
                , VerboseKey
"    " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> VerboseKey
forall a. Show a => a -> VerboseKey
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 (VerboseKey, Type)]
tel = Int -> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. Int -> [a] -> [a]
take Int
pIndex ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)])
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList (Tele (Dom Type) -> [Dom (VerboseKey, Type)])
-> Tele (Dom Type) -> [Dom (VerboseKey, 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 (VerboseKey, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom (VerboseKey, 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 :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> 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 VerboseKey] -> ProjLams
ProjLams ([Arg VerboseKey] -> ProjLams) -> [Arg VerboseKey] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Arg VerboseKey)
-> [Dom (VerboseKey, Type)] -> [Arg VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term VerboseKey -> Arg VerboseKey
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term VerboseKey -> Arg VerboseKey)
-> (Dom (VerboseKey, Type) -> Dom' Term VerboseKey)
-> Dom (VerboseKey, Type)
-> Arg VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VerboseKey, Type) -> VerboseKey)
-> Dom (VerboseKey, Type) -> Dom' Term VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst) [Dom (VerboseKey, Type)]
tel
                    }
              let newDef :: Defn
newDef = Defn
def
                           { funProjection :: Maybe Projection
funProjection     = Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
projection
                           , funClauses :: [Clause]
funClauses        = [Clause]
cls'
                           , funSplitTree :: Maybe SplitTree
funSplitTree      = Maybe SplitTree
st
                           , funCompiled :: Maybe CompiledClauses
funCompiled       = Maybe CompiledClauses
cc
                           , funInv :: FunctionInverse
funInv            = Int -> FunctionInverse -> FunctionInverse
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n (FunctionInverse -> FunctionInverse)
-> FunctionInverse -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Defn -> FunctionInverse
funInv Defn
def
                           }
              QName -> Definition -> TCM ()
addConstant QName
x (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ Definition
defn { defPolarity :: [Polarity]
defPolarity       = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
n ([Polarity] -> [Polarity]) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> a -> b
$ Definition -> [Polarity]
defPolarity Definition
defn
                                   , defArgOccurrences :: [Occurrence]
defArgOccurrences = Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
drop Int
n ([Occurrence] -> [Occurrence]) -> [Occurrence] -> [Occurrence]
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{}} ->
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  injective functions can't be projections"
    Function{funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
AbstractDef} ->
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  abstract functions can't be projections"
    Function{funProjection :: Defn -> Maybe Projection
funProjection = Just{}} ->
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  already projection like"
    Function{funMutual :: Defn -> Maybe [QName]
funMutual = Just (QName
_:[QName]
_)} ->
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  mutual functions can't be projections"
    Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
Nothing} ->
      VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  mutuality check has not run yet"
    Axiom{}        -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but Axiom"
    DataOrRecSig{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but DataOrRecSig"
    GeneralizableVar{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but GeneralizableVar"
    AbstractDefn{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but AbstractDefn"
    Constructor{}  -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but Constructor"
    Datatype{}     -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but Datatype"
    Primitive{}    -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but Primitive"
    PrimitiveSort{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  not a function, but PrimitiveSort"
    Record{}       -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.proj.like" Int
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  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 (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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- recursive occurrence
        Maybe Integer
_               -> Bool -> TCMT IO Bool
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 (Pattern' DBPatVar)] -> Bool
forall x. Int -> [NamedArg (Pattern' x)] -> Bool
onlyMatch Int
n [NamedArg (Pattern' DBPatVar)]
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 (Pattern' DBPatVar)]
ps       = Clause -> [NamedArg (Pattern' DBPatVar)]
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 (Pattern' DBPatVar) -> [Arg (Either DBPatVar Term)])
-> [NamedArg (Pattern' DBPatVar)] -> [Arg (Either DBPatVar Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NamedArg (Pattern' DBPatVar) -> [Arg (Either DBPatVar Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' DBPatVar)]
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 (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 (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 VerboseKey
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