{- |

"Injectivity", or more precisely, "constructor headedness", is a
property of functions defined by pattern matching that helps us solve
constraints involving blocked applications of such functions.
"Blocked" shall mean here that pattern matching is blocked on a meta
variable, and constructor headedness lets us learn more about that
meta variable.

Consider the simple example:
@
  isZero : Nat -> Bool
  isZero zero    = true
  isZero (suc n) = false
@
This function is constructor-headed, meaning that all rhss are headed
by a distinct constructor.  Thus, on a constraint like
@
  isZero ?X = false : Bool
@
involving an application of @isZero@ that is blocked on meta variable @?X@,
we can exploit injectivity and learn that @?X = suc ?Y@ for a new
meta-variable @?Y@.

Which functions qualify for injectivity?

1. The function needs to have at least one non-absurd clause that has
a proper match, meaning that the function can actually be blocked on a
meta.  Proper matches are these patterns:

  - data constructor (@ConP@, but not record constructor)
  - literal (@LitP@)
  - HIT-patterns (@DefP@)

Projection patterns (@ProjP@) are excluded because metas cannot occupy their place!

2. All the clauses that satisfy (1.) need to be headed by a distinct constructor.

-}

module Agda.TypeChecking.Injectivity where

import Control.Applicative
import Control.Monad
import Control.Monad.Except
import Control.Monad.Fail
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Trans.Maybe

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.Traversable hiding (for)
import Data.Semigroup ((<>))
import Data.Foldable (fold)

import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance (isIrrelevantOrPropM)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Primitive.Base
import Agda.TypeChecking.Primitive.Cubical
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Warnings

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.ProfileOptions as Profile

import Agda.Utils.Impossible

headSymbol :: Term -> TCM (Maybe TermHead)
headSymbol :: Term -> TCM (Maybe TermHead)
headSymbol Term
v = do -- ignoreAbstractMode $ do
  -- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage

  Term
v <- forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t a. Blocked' t a -> a
ignoreBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Term -> m (Blocked Term)
reduceHead Term
v
  case Term
v of
    Def QName
f Elims
_ -> do
      let yes :: TCM (Maybe TermHead)
yes = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
f
          no :: TCMT IO (Maybe a)
no  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
        -- Andreas, 2013-02-18
        -- if we do not ignoreAbstractMode here, abstract Functions get turned
        -- into Axioms, but we want to distinguish these.
      case Defn
def of
        Datatype{}  -> TCM (Maybe TermHead)
yes
        Record{}    -> TCM (Maybe TermHead)
yes
        DataOrRecSig{} -> TCM (Maybe TermHead)
yes
        Axiom{}     -> do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.axiom" Nat
50 forall a b. (a -> b) -> a -> b
$ [Char]
"headSymbol: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ [Char]
" is an Axiom."
          -- Don't treat axioms in the current mutual block
          -- as constructors (they might have definitions we
          -- don't know about yet).
          forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) TCM (Maybe TermHead)
yes forall a b. (a -> b) -> a -> b
$ \ MutualId
mb -> do
            Set QName
fs <- MutualBlock -> Set QName
mutualNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
mb
            if forall a. Ord a => a -> Set a -> Bool
Set.member QName
f Set QName
fs then forall {a}. TCMT IO (Maybe a)
no else TCM (Maybe TermHead)
yes
        Function{}    -> forall {a}. TCMT IO (Maybe a)
no
        Primitive{}   -> forall {a}. TCMT IO (Maybe a)
no
        PrimitiveSort{} -> forall {a}. TCMT IO (Maybe a)
no
        GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Constructor{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        AbstractDefn{}-> forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Andreas, 2019-07-10, issue #3900: canonicalName needs ignoreAbstractMode
    Con ConHead
c ConInfo
_ Elims
_ -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
                 QName
q <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
                 forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
q) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
                     {- else -}     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
q
    Sort Sort
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just TermHead
SortHead)
    Pi Dom Type
_ Abs Type
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just TermHead
PiHead)
    Var Nat
i [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> TermHead
VarHead Nat
i) -- Only naked variables. Otherwise substituting a neutral term is not guaranteed to stay neutral.
    Lit Literal
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing -- TODO: LitHead (for literals with no constructorForm)
    Lam{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Var{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Level{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    MetaV{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    DontCare{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Dummy [Char]
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

-- | Is this a matchable definition, or constructor, which reduces based
-- on interval substitutions?
isUnstableDef :: PureTCM m => QName -> m Bool
isUnstableDef :: forall (m :: * -> *). PureTCM m => QName -> m Bool
isUnstableDef QName
qn = do
  Definition
defn <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
  [Maybe QName]
prims <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName'
    [ [Char]
builtinHComp
    , [Char]
builtinComp
    , [Char]
builtinTrans
    , [Char]
builtinGlue
    , [Char]
builtin_glue
    , [Char]
builtin_glueU ]
  case Definition -> Defn
theDef Definition
defn of
    Defn
_ | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. a -> Maybe a
Just QName
qn forall a. Eq a => a -> a -> Bool
==) [Maybe QName]
prims -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Function{funIsKanOp :: Defn -> Maybe QName
funIsKanOp = Just QName
_} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Defn
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False


-- | Do a full whnf and treat neutral terms as rigid. Used on the arguments to
--   an injective functions and to the right-hand side. Only returns
--   heads which are stable under interval substitution, i.e. NOT path
--   constructors or generated hcomp/transp!
headSymbol'
  :: (PureTCM m, MonadError TCErr m)
  => Term -> m (Maybe TermHead)
headSymbol' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m (Maybe TermHead)
headSymbol' Term
v = do
  Blocked Term
v <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
  case Blocked Term
v of
    Blocked{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    NotBlocked NotBlocked' Term
_ Term
v -> case Term
v of
      Def QName
g Elims
_    ->
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). PureTCM m => QName -> m Bool
isUnstableDef QName
g)
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing)
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
g)
      Con ConHead
c ConInfo
_ Elims
_  -> do
        QName
q <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
q)
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing)
          (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
q)
      Var Nat
i Elims
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Nat -> TermHead
VarHead Nat
i)
      Sort Sort
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just TermHead
SortHead
      Pi Dom Type
_ Abs Type
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just TermHead
PiHead
      Lit Literal
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Lam{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Level{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      DontCare{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      MetaV{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Dummy [Char]
s Elims
_  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

-- | Does deBruijn variable i correspond to a top-level argument, and if so
--   which one (index from the left).
topLevelArg :: Clause -> Int -> Maybe TermHead
topLevelArg :: Clause -> Nat -> Maybe TermHead
topLevelArg Clause{ namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps } Nat
i =
  case [ Nat
n | (Nat
n, VarP PatternInfo
_ (DBPatVar [Char]
_ Nat
j)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
0..] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs
ps, Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j ] of
    []    -> forall a. Maybe a
Nothing
    [Nat
n]   -> forall a. a -> Maybe a
Just (Nat -> TermHead
VarHead Nat
n)
    Nat
_:Nat
_:[Nat]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Join a list of inversion maps.
joinHeadMaps :: [InversionMap c] -> InversionMap c
joinHeadMaps :: forall c. [InversionMap c] -> InversionMap c
joinHeadMaps = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Semigroup a => a -> a -> a
(<>)

-- | Update the heads of an inversion map.
updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c)
updateHeads :: forall (m :: * -> *) c.
Monad m =>
(TermHead -> [c] -> m TermHead)
-> InversionMap c -> m (InversionMap c)
updateHeads TermHead -> [c] -> m TermHead
f InversionMap c
m = forall c. [InversionMap c] -> InversionMap c
joinHeadMaps forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TermHead, [c]) -> m (InversionMap c)
f' (forall k a. Map k a -> [(k, a)]
Map.toList InversionMap c
m)
  where f' :: (TermHead, [c]) -> m (InversionMap c)
f' (TermHead
h, [c]
c) = (forall k a. k -> a -> Map k a
`Map.singleton` [c]
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermHead -> [c] -> m TermHead
f TermHead
h [c]
c

checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
checkInjectivity QName
f [Clause]
cs0
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
properlyMatchingClause [Clause]
cs) = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check.pointless" Nat
35 forall a b. (a -> b) -> a -> b
$
        [Char]
"Injectivity of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (QName -> QName
A.qnameToConcrete QName
f) forall a. [a] -> [a] -> [a]
++ [Char]
" would be pointless."
      forall (m :: * -> *) a. Monad m => a -> m a
return forall c. FunctionInverse' c
NotInjective
  | Bool
otherwise = QName -> [Clause] -> TCM FunctionInverse
checkInjectivity' QName
f [Clause]
cs
  where
    -- We can filter out absurd clauses.
    cs :: [Clause]
cs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cs0
    -- We cannot filter out clauses that have no proper match, because
    -- these could be catch-all clauses.
    -- However, we need at least one proper match to get injectivity started.
    properlyMatchingClause :: Clause -> Bool
properlyMatchingClause =
      forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
False Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats

-- | Precondition: all the given clauses are non-absurd and contain a proper match.
checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse
checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse
checkInjectivity' QName
f [Clause]
cs = forall a. a -> Maybe a -> a
fromMaybe forall c. FunctionInverse' c
NotInjective forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"Checking injectivity of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f

  let varToArg :: Clause -> TermHead -> MaybeT TCM TermHead
      varToArg :: Clause -> TermHead -> MaybeT (TCMT IO) TermHead
varToArg Clause
c (VarHead Nat
i) = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Clause -> Nat -> Maybe TermHead
topLevelArg Clause
c Nat
i
      varToArg Clause
_ TermHead
h           = forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h

  -- We don't need to consider absurd clauses
  let computeHead :: Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]]
computeHead Clause
c | NAPs -> Bool
hasDefP (Clause -> NAPs
namedClausePats Clause
c) = forall (m :: * -> *) a. Monad m => a -> m a
return []
      -- hasDefP clauses are skipped, these matter only for --cubical, in which case the function will behave as NotInjective.
      computeHead c :: Clause
c@Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Just Term
body , clauseType :: Clause -> Maybe (Arg Type)
clauseType = Just Arg Type
tbody } = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) forall a b. (a -> b) -> a -> b
$ do
        Bool
maybeIrr <- forall a b. (a -> b) -> Either a b -> b
fromRight (forall a b. a -> b -> a
const Bool
True) forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Arg Type
tbody
        -- We treat ordinary clauses with IApply copatterns as *immediately*
        -- failing the injectivity check. Consider e.g.
        --   foo x = T
        --   foo (y i) = Glue U λ { (i = i0) → T , _ ; (i = i1) → T , _ }
        -- seeing foo α = Glue ... and inverting it to α = y β loses solutions. E.g. if we
        -- later had some other α = x, now we're screwed, x ≠ y β. But if we had postponed
        -- originally we'd just compare T = Glue ... which has a chance of going through.
        let ivars :: [Nat]
ivars = forall p. IApplyVars p => p -> [Nat]
iApplyVars (Clause -> NAPs
namedClausePats Clause
c)
        forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
ivars)
        TermHead
h <- if Bool
maybeIrr then forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
UnknownHead else
          Clause -> TermHead -> MaybeT (TCMT IO) TermHead
varToArg Clause
c forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe TermHead
UnknownHead forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              Term -> TCM (Maybe TermHead)
headSymbol Term
body
        forall (m :: * -> *) a. Monad m => a -> m a
return [forall k a. k -> a -> Map k a
Map.singleton TermHead
h [Clause
c]]
      computeHead Clause
_ = forall (m :: * -> *) a. Monad m => a -> m a
return []

  Map TermHead [Clause]
hdMap <- forall c. [InversionMap c] -> InversionMap c
joinHeadMaps forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]]
computeHead [Clause]
cs

  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TermHead
UnknownHead Map TermHead [Clause]
hdMap of
    Just (Clause
_:Clause
_:[Clause]
_) -> forall (f :: * -> *) a. Alternative f => f a
empty -- More than one unknown head: we can't really do anything in that case.
    Maybe [Clause]
_            -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn  [Char]
"tc.inj.check" Nat
20 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ [Char]
" is potentially injective."
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.check" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall k a. Map k a -> [(k, a)]
Map.toList Map TermHead [Clause]
hdMap) forall a b. (a -> b) -> a -> b
$ \ (TermHead
h, [Clause]
uc) ->
      forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Pretty a => a -> [Char]
prettyShow TermHead
h) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"-->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      case [Clause]
uc of
        [Clause
c] -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
c
        [Clause]
_   -> TCMT IO Doc
"(multiple clauses)"
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c. InversionMap c -> FunctionInverse' c
Inverse Map TermHead [Clause]
hdMap

-- | If a clause is over-applied we can't trust the head (Issue 2944). For
--   instance, the clause might be `f ps = u , v` and the actual call `f vs
--   .fst`. In this case the head will be the head of `u` rather than `_,_`.
checkOverapplication
  :: forall m. (HasConstInfo m)
  => Elims -> InversionMap Clause -> m (InversionMap Clause)
checkOverapplication :: forall (m :: * -> *).
HasConstInfo m =>
Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
checkOverapplication Elims
es = forall (m :: * -> *) c.
Monad m =>
(TermHead -> [c] -> m TermHead)
-> InversionMap c -> m (InversionMap c)
updateHeads TermHead -> [Clause] -> m TermHead
overapplied
  where
    overapplied :: TermHead -> [Clause] -> m TermHead
    overapplied :: TermHead -> [Clause] -> m TermHead
overapplied TermHead
h [Clause]
cs | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
isOverapplied) [Clause]
cs = forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h
    overapplied TermHead
h [Clause]
cs = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall {m :: * -> *}. HasConstInfo m => TermHead -> m Bool
isSuperRigid TermHead
h) (forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h) (forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
UnknownHead)

    -- A super-rigid head is one that can't be eliminated. Crucially, this is
    -- applied after instantiateVars, so VarHeads are really bound variables.
    isSuperRigid :: TermHead -> m Bool
isSuperRigid TermHead
SortHead     = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
PiHead       = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid VarHead{}    = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
UnknownHead  = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- or False, doesn't matter
    isSuperRigid (ConsHead QName
q) = do
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
def of
        Axiom{}        -> Bool
True
        DataOrRecSig{} -> Bool
True
        AbstractDefn{} -> Bool
True
        Function{}     -> Bool
False
        Datatype{}     -> Bool
True
        Record{}       -> Bool
True
        Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead{ conDataRecord :: ConHead -> DataOrRecord
conDataRecord = DataOrRecord
d, conFields :: ConHead -> [Arg QName]
conFields = [Arg QName]
fs }}
                       -> DataOrRecord
d forall a. Eq a => a -> a -> Bool
== DataOrRecord
IsData Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Arg QName]
fs   -- Record constructors can be eliminated by projections
        Primitive{}    -> Bool
False
        PrimitiveSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__


    isOverapplied :: Clause -> Bool
isOverapplied Clause{ namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps } = forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Nat
length NAPs
ps

-- | Turn variable heads, referring to top-level argument positions, into
--   proper heads. These might still be `VarHead`, but in that case they refer to
--   deBruijn variables. Checks that the instantiated heads are still rigid and
--   distinct.
instantiateVarHeads
  :: forall m c. (PureTCM m, MonadError TCErr m)
  => QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
instantiateVarHeads :: forall (m :: * -> *) c.
(PureTCM m, MonadError TCErr m) =>
QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
instantiateVarHeads QName
f Elims
es InversionMap c
m = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) c.
Monad m =>
(TermHead -> [c] -> m TermHead)
-> InversionMap c -> m (InversionMap c)
updateHeads (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermHead -> MaybeT m TermHead
instHead) InversionMap c
m
  where
    instHead :: TermHead -> MaybeT m TermHead
    instHead :: TermHead -> MaybeT m TermHead
instHead h :: TermHead
h@(VarHead Nat
i)
      | Just (Apply Arg Term
arg) <- Elims
es forall a. [a] -> Nat -> Maybe a
!!! Nat
i = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m (Maybe TermHead)
headSymbol' (forall e. Arg e -> e
unArg Arg Term
arg)
      | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty   -- impossible?
    instHead TermHead
h = forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h

-- | Argument should be in weak head normal form.
functionInverse
  :: (PureTCM m, MonadError TCErr m)
  => Term -> m InvView
functionInverse :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m InvView
functionInverse = \case
  Def QName
f Elims
es -> do
    FunctionInverse
inv <- Definition -> FunctionInverse
defInverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
    Maybe Cubical
cubical <- PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    case FunctionInverse
inv of
      FunctionInverse
NotInjective -> forall (m :: * -> *) a. Monad m => a -> m a
return InvView
NoInv
      Inverse Map TermHead [Clause]
m -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe InvView
NoInv (QName -> Elims -> Map TermHead [Clause] -> InvView
Inv QName
f Elims
es) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *).
HasConstInfo m =>
Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
checkOverapplication Elims
es) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) c.
(PureTCM m, MonadError TCErr m) =>
QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
instantiateVarHeads QName
f Elims
es Map TermHead [Clause]
m)
        -- NB: Invertible functions are never classified as
        --     projection-like, so this is fine, we are not
        --     missing parameters.  (Andreas, 2013-11-01)
  Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return InvView
NoInv

data InvView = Inv QName [Elim] (InversionMap Clause)
             | NoInv

-- | Precondition: The first term must be blocked on the given meta and the second must be neutral.
useInjectivity :: MonadConversion m => CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
useInjectivity :: forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
useInjectivity CompareDirection
dir Blocker
blocker CompareAs
ty Term
blk Term
neu = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Nat TCEnv
eInjectivityDepth forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ do
  InvView
inv <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m InvView
functionInverse Term
blk
  -- Injectivity might cause non-termination for unsatisfiable constraints
  -- (#431, #3067). Look at the number of active problems and the injectivity
  -- depth to detect this.
  Nat
nProblems <- forall a. Set a -> Nat
Set.size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Set ProblemId) TCEnv
eActiveProblems
  Nat
injDepth  <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Nat TCEnv
eInjectivityDepth
  let depth :: Nat
depth = forall a. Ord a => a -> a -> a
max Nat
nProblems Nat
injDepth
  Nat
maxDepth  <- forall (m :: * -> *). HasOptions m => m Nat
maxInversionDepth
  case InvView
inv of
    InvView
NoInv            -> m ()
fallback  -- not invertible
    Inv QName
f Elims
blkArgs Map TermHead [Clause]
hdMap
      | Nat
depth forall a. Ord a => a -> a -> Bool
> Nat
maxDepth -> forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (QName -> Warning
InversionDepthReached QName
f) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
fallback
      | Bool
otherwise -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"useInjectivity on" forall a. [a] -> [a] -> [a]
++
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
blk, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
neu, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM CompareAs
ty]
      forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"compare by reduction: injectivity"
      let canReduceToSelf :: Bool
canReduceToSelf = forall k a. Ord k => k -> Map k a -> Bool
Map.member (QName -> TermHead
ConsHead QName
f) Map TermHead [Clause]
hdMap Bool -> Bool -> Bool
|| forall k a. Ord k => k -> Map k a -> Bool
Map.member TermHead
UnknownHead Map TermHead [Clause]
hdMap
      case Term
neu of
        -- f us == f vs  <=>  us == vs
        -- Crucially, this relies on `f vs` being neutral and only works
        -- if `f` is not a possible head for `f us`.
        Def QName
f' Elims
neuArgs | QName
f forall a. Eq a => a -> a -> Bool
== QName
f', Bool -> Bool
not Bool
canReduceToSelf -> do
          Type
fTy <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"comparing application of injective function" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f] forall a. [a] -> [a] -> [a]
++
                  forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"at")
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
neuArgs
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"and type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fTy
            ]
          [IsForced]
fs  <- forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
f
          [Polarity]
pol <- forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
cmp QName
f
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert.success" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"Successful spine comparison of", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f]
          forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"compare by reduction: injectivity successful"
          forall {a} {b}. (a -> a -> b) -> a -> a -> b
app (forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pol [IsForced]
fs Type
fTy (QName -> Elims -> Term
Def QName
f [])) Elims
blkArgs Elims
neuArgs

        -- f us == c vs
        --    Find the clause unique clause `f ps` with head `c` and unify
        --    us == ps  with fresh metas for the pattern variables of ps.
        --    If there's no such clause we can safely throw an error.
        Term
_ -> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m (Maybe TermHead)
headSymbol' Term
neu forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
          Maybe TermHead
Nothing -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"no head symbol found for" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
neu] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
", so not inverting"
            m ()
fallback
          Just (ConsHead QName
f') | QName
f forall a. Eq a => a -> a -> Bool
== QName
f', Bool
canReduceToSelf -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"head symbol" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f'] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can reduce to self, so not inverting"
            m ()
fallback
                                    -- We can't invert in this case, since we can't
                                    -- tell the difference between a solution that makes
                                    -- the blocked term neutral and one that makes progress.
          Just TermHead
hd -> forall (m :: * -> *).
MonadConversion m =>
Comparison
-> Term
-> InvView
-> TermHead
-> m ()
-> m ()
-> (Term -> m ())
-> m ()
invertFunction Comparison
cmp Term
blk InvView
inv TermHead
hd m ()
fallback m ()
err Term -> m ()
success
            where err :: m ()
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ forall {a} {b}. (a -> a -> b) -> a -> a -> b
app (\ Term
u Term
v -> Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
ty) Term
blk Term
neu
  where
    fallback :: m ()
fallback     = forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker forall a b. (a -> b) -> a -> b
$ forall {a} {b}. (a -> a -> b) -> a -> a -> b
app (Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp CompareAs
ty) Term
blk Term
neu
    success :: Term -> m ()
success Term
blk' = forall {a} {b}. (a -> a -> b) -> a -> a -> b
app (forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
ty) Term
blk' Term
neu

    cmpApp :: (Comparison, (a -> a -> b) -> a -> a -> b)
    cmpApp :: forall a b. (Comparison, (a -> a -> b) -> a -> a -> b)
cmpApp = case CompareDirection
dir of
      CompareDirection
DirEq -> (Comparison
CmpEq, forall a. a -> a
id)
      CompareDirection
DirLeq -> (Comparison
CmpLeq, forall a. a -> a
id)
      CompareDirection
DirGeq -> (Comparison
CmpLeq, forall a b c. (a -> b -> c) -> b -> a -> c
flip)
    (Comparison
cmp, (a -> a -> b) -> a -> a -> b
app) = forall a b. (Comparison, (a -> a -> b) -> a -> a -> b)
cmpApp

-- | The second argument should be a blocked application and the third argument
--   the inverse of the applied function.
invertFunction
  :: MonadConversion m
  => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m ()
invertFunction :: forall (m :: * -> *).
MonadConversion m =>
Comparison
-> Term
-> InvView
-> TermHead
-> m ()
-> m ()
-> (Term -> m ())
-> m ()
invertFunction Comparison
_ Term
_ InvView
NoInv TermHead
_ m ()
fallback m ()
_ Term -> m ()
_ = m ()
fallback
invertFunction Comparison
cmp Term
blk (Inv QName
f Elims
blkArgs Map TermHead [Clause]
hdMap) TermHead
hd m ()
fallback m ()
err Term -> m ()
success = do
    Type
fTy <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"inverting injective function" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fTy]
      , TCMT IO Doc
"for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs)
      ]                         -- Clauses with unknown heads are also possible candidates
    case forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TermHead
hd Map TermHead [Clause]
hdMap forall a. Semigroup a => a -> a -> a
<> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TermHead
UnknownHead Map TermHead [Clause]
hdMap of
      [] -> m ()
err
      Clause
_:Clause
_:[Clause]
_ -> m ()
fallback
      [cl :: Clause
cl@Clause{ clauseTel :: Clause -> Telescope
clauseTel  = Telescope
tel }] -> forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas m ()
fallback forall a b. (a -> b) -> a -> b
$ do
          let ps :: [Arg DeBruijnPattern]
ps   = Clause -> [Arg DeBruijnPattern]
clausePats Clause
cl
              perm :: Permutation
perm = 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
          -- These are what dot patterns should be instantiated at
          [Term]
ms <- forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
newTelMeta Telescope
tel
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"meta patterns" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
ms)
            , TCMT IO Doc
"  perm =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Permutation
perm)
            , TCMT IO Doc
"  tel  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
            , TCMT IO Doc
"  ps   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Arg DeBruijnPattern]
ps)
            ]
          -- and this is the order the variables occur in the patterns
          let msAux :: [Term]
msAux = forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
invertP forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
perm) [Term]
ms
          let sub :: Substitution' Term
sub   = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall a. [a] -> [a]
reverse [Term]
ms)
          Elims
margs <- forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 HasConstInfo m, MonadFail m) =>
Arg DeBruijnPattern -> m Elim
metaElim [Arg DeBruijnPattern]
ps) [Term]
msAux) Substitution' Term
sub
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"inversion"
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"lhs  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
margs
              , TCMT IO Doc
"rhs  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs
              , TCMT IO Doc
"type =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fTy
              ]
            ]
          -- Since we do not care for the value of non-variant metas here,
          -- we can treat 'Nonvariant' as 'Invariant'.
          -- That ensures these metas do not remain unsolved.
          [Polarity]
pol <- [Polarity] -> [Polarity]
purgeNonvariant forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
cmp QName
f
          [IsForced]
fs  <- forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
f
          -- The clause might not give as many patterns as there
          -- are arguments (point-free style definitions).
          let blkArgs' :: Elims
blkArgs' = forall a. Nat -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
margs) Elims
blkArgs
          forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pol [IsForced]
fs Type
fTy (QName -> Elims -> Term
Def QName
f []) Elims
margs Elims
blkArgs'

          -- Check that we made progress.
          Reduced (Blocked Term) Term
r <- forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ Bool
-> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep Bool
False (QName -> Elims -> Term
Def QName
f []) QName
f Elims
blkArgs
          case Reduced (Blocked Term) Term
r of
            YesReduction Simplification
_ Term
blk' -> do
              forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert.success" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"Successful inversion of", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f, TCMT IO Doc
"at", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd]
              KeepMetas
KeepMetas forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> m ()
success Term
blk'
            NoReduction{}       -> do
              forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ TCMT IO Doc
"aborting inversion;" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
blk
                , TCMT IO Doc
"does not reduce"
                ]
              forall (m :: * -> *) a. Monad m => a -> m a
return KeepMetas
RollBackMetas
  where
    nextMeta :: (MonadState [Term] m, MonadFail m) => m Term
    nextMeta :: forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
nextMeta = do
      Term
m : [Term]
ms <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put [Term]
ms
      forall (m :: * -> *) a. Monad m => a -> m a
return Term
m

    dotP :: MonadReader Substitution m => Term -> m Term
    dotP :: forall (m :: * -> *).
MonadReader (Substitution' Term) m =>
Term -> m Term
dotP Term
v = do
      Substitution' Term
sub <- forall r (m :: * -> *). MonadReader r m => m r
ask
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub Term
v

    metaElim
      :: (MonadState [Term] m, MonadReader Substitution m, HasConstInfo m, MonadFail m)
      => Arg DeBruijnPattern -> m Elim
    metaElim :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 HasConstInfo m, MonadFail m) =>
Arg DeBruijnPattern -> m Elim
metaElim (Arg ArgInfo
_ (ProjP ProjOrigin
o QName
p))  = forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
p
    metaElim (Arg ArgInfo
info DeBruijnPattern
p)         = forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
DeBruijnPattern -> m Term
metaPat DeBruijnPattern
p

    metaArgs
      :: (MonadState [Term] m, MonadReader Substitution m, MonadFail m)
      => [NamedArg DeBruijnPattern] -> m Args
    metaArgs :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
NAPs -> m Args
metaArgs NAPs
args = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
DeBruijnPattern -> m Term
metaPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing) NAPs
args

    metaPat
      :: (MonadState [Term] m, MonadReader Substitution m, MonadFail m)
      => DeBruijnPattern -> m Term
    metaPat :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
DeBruijnPattern -> m Term
metaPat (DotP PatternInfo
_ Term
v)       = forall (m :: * -> *).
MonadReader (Substitution' Term) m =>
Term -> m Term
dotP Term
v
    metaPat (VarP PatternInfo
_ DBPatVar
_)       = forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
nextMeta
    metaPat (IApplyP{})      = forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
nextMeta
    metaPat (ConP ConHead
c ConPatternInfo
mt NAPs
args) = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c (ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
mt) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
NAPs -> m Args
metaArgs NAPs
args
    metaPat (DefP PatternInfo
o QName
q NAPs
args)  = QName -> Elims -> Term
Def QName
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
NAPs -> m Args
metaArgs NAPs
args
    metaPat (LitP PatternInfo
_ Literal
l)       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    metaPat ProjP{}          = forall a. HasCallStack => a
__IMPOSSIBLE__

forcePiUsingInjectivity :: Type -> TCM Type
forcePiUsingInjectivity :: Type -> TCM Type
forcePiUsingInjectivity Type
t = forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
    Blocked Blocker
_ Type
blkTy -> do
      let blk :: Term
blk = forall t a. Type'' t a -> a
unEl Type
blkTy
      InvView
inv <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m InvView
functionInverse Term
blk
      Type
blkTy forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
MonadConversion m =>
Comparison
-> Term
-> InvView
-> TermHead
-> m ()
-> m ()
-> (Term -> m ())
-> m ()
invertFunction Comparison
CmpEq Term
blk InvView
inv TermHead
PiHead TCMT IO ()
fallback TCMT IO ()
err forall {m :: * -> *} {p}. Monad m => p -> m ()
success
    NotBlocked NotBlocked' Term
_ Type
t -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
  where
    fallback :: TCMT IO ()
fallback  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    err :: TCMT IO ()
err       = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (Type -> TypeError
ShouldBePi Type
t)
    success :: p -> m ()
success p
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()