{- |

"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.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 qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

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

-- | Do a full whnf and treat neutral terms as rigid. Used on the arguments to
--   an injective functions and to the right-hand side.
headSymbol'
  :: (PureTCM m, MonadError TCErr m)
  => Term -> m (Maybe TermHead)
headSymbol' :: Term -> m (Maybe TermHead)
headSymbol' Term
v = do
  Blocked' Term Term
v <- (Term -> m Term) -> Blocked' Term Term -> m (Blocked' Term Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Blocked' Term Term -> m (Blocked' Term Term))
-> m (Blocked' Term Term) -> m (Blocked' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> m (Blocked' Term Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
  case Blocked' Term Term
v of
    Blocked{} -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    NotBlocked NotBlocked' Term
_ Term
v -> case Term
v of
      Def QName
g Elims
_    -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TermHead -> m (Maybe TermHead))
-> Maybe TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (TermHead -> Maybe TermHead) -> TermHead -> Maybe TermHead
forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
g
      Con ConHead
c ConInfo
_ Elims
_  -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TermHead -> m (Maybe TermHead))
-> Maybe TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (TermHead -> Maybe TermHead) -> TermHead -> Maybe TermHead
forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead (QName -> TermHead) -> QName -> TermHead
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
      Var VerboseLevel
i Elims
_    -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TermHead -> m (Maybe TermHead))
-> Maybe TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (VerboseLevel -> TermHead
VarHead VerboseLevel
i)
      Sort Sort
_     -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TermHead -> m (Maybe TermHead))
-> Maybe TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just TermHead
SortHead
      Pi Dom Type
_ Abs Type
_     -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TermHead -> m (Maybe TermHead))
-> Maybe TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just TermHead
PiHead
      Lit Literal
_      -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      Lam{}      -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      Level{}    -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      DontCare{} -> Maybe TermHead -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      MetaV{}    -> m (Maybe TermHead)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Dummy VerboseKey
s Elims
_  -> VerboseKey -> m (Maybe TermHead)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
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 -> VerboseLevel -> Maybe TermHead
topLevelArg Clause{ namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps } VerboseLevel
i =
  case [ VerboseLevel
n | (VerboseLevel
n, VarP PatternInfo
_ (DBPatVar VerboseKey
_ VerboseLevel
j)) <- [VerboseLevel]
-> [DeBruijnPattern] -> [(VerboseLevel, DeBruijnPattern)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] ([DeBruijnPattern] -> [(VerboseLevel, DeBruijnPattern)])
-> [DeBruijnPattern] -> [(VerboseLevel, DeBruijnPattern)]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NAPs
ps, VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j ] of
    []    -> Maybe TermHead
forall a. Maybe a
Nothing
    [VerboseLevel
n]   -> TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (VerboseLevel -> TermHead
VarHead VerboseLevel
n)
    VerboseLevel
_:VerboseLevel
_:[VerboseLevel]
_ -> Maybe TermHead
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Join a list of inversion maps.
joinHeadMaps :: [InversionMap c] -> InversionMap c
joinHeadMaps :: [InversionMap c] -> InversionMap c
joinHeadMaps = ([c] -> [c] -> [c]) -> [InversionMap c] -> InversionMap c
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [c] -> [c] -> [c]
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 :: (TermHead -> [c] -> m TermHead)
-> InversionMap c -> m (InversionMap c)
updateHeads TermHead -> [c] -> m TermHead
f InversionMap c
m = [InversionMap c] -> InversionMap c
forall c. [InversionMap c] -> InversionMap c
joinHeadMaps ([InversionMap c] -> InversionMap c)
-> m [InversionMap c] -> m (InversionMap c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TermHead, [c]) -> m (InversionMap c))
-> [(TermHead, [c])] -> m [InversionMap c]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TermHead, [c]) -> m (InversionMap c)
f' (InversionMap c -> [(TermHead, [c])]
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) = (TermHead -> [c] -> InversionMap c
forall k a. k -> a -> Map k a
`Map.singleton` [c]
c) (TermHead -> InversionMap c) -> m TermHead -> m (InversionMap 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 ((Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
properlyMatchingClause [Clause]
cs) = do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.check.pointless" VerboseLevel
35 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        VerboseKey
"Injectivity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (QName -> QName
A.qnameToConcrete QName
f) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" would be pointless."
      FunctionInverse -> TCM FunctionInverse
forall (m :: * -> *) a. Monad m => a -> m a
return FunctionInverse
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 = (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
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 =
      (NamedArg DeBruijnPattern -> Bool) -> NAPs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool -> DeBruijnPattern -> Bool
forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
False Bool
False (DeBruijnPattern -> Bool)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) (NAPs -> Bool) -> (Clause -> NAPs) -> Clause -> Bool
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 = FunctionInverse -> Maybe FunctionInverse -> FunctionInverse
forall a. a -> Maybe a -> a
fromMaybe FunctionInverse
forall c. FunctionInverse' c
NotInjective (Maybe FunctionInverse -> FunctionInverse)
-> (MaybeT TCM FunctionInverse -> TCM (Maybe FunctionInverse))
-> MaybeT TCM FunctionInverse
-> TCM FunctionInverse
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MaybeT TCM FunctionInverse -> TCM (Maybe FunctionInverse)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM FunctionInverse -> TCM FunctionInverse)
-> MaybeT TCM FunctionInverse -> TCM FunctionInverse
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> VerboseKey -> MaybeT TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.inj.check" VerboseLevel
40 (VerboseKey -> MaybeT TCM ()) -> VerboseKey -> MaybeT TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Checking injectivity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
f

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

  -- We don't need to consider absurd clauses
  let computeHead :: Clause -> MaybeT TCM [Map TermHead [Clause]]
computeHead c :: Clause
c@Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Just Term
body , clauseType :: Clause -> Maybe (Arg Type)
clauseType = Just Arg Type
tbody } = do
        Bool
maybeIrr <- (Blocker -> Bool) -> Either Blocker Bool -> Bool
forall a b. (a -> b) -> Either a b -> b
fromRight (Bool -> Blocker -> Bool
forall a b. a -> b -> a
const Bool
True) (Either Blocker Bool -> Bool)
-> (BlockT (MaybeT TCM) Bool -> MaybeT TCM (Either Blocker Bool))
-> BlockT (MaybeT TCM) Bool
-> MaybeT TCM Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BlockT (MaybeT TCM) Bool -> MaybeT TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (MaybeT TCM) Bool -> MaybeT TCM Bool)
-> BlockT (MaybeT TCM) Bool -> MaybeT TCM Bool
forall a b. (a -> b) -> a -> b
$ Arg Type -> BlockT (MaybeT TCM) Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Arg Type
tbody
        TermHead
h <- if Bool
maybeIrr then TermHead -> MaybeT TCM TermHead
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
UnknownHead else
          Clause -> TermHead -> MaybeT TCM TermHead
varToArg Clause
c (TermHead -> MaybeT TCM TermHead)
-> MaybeT TCM TermHead -> MaybeT TCM TermHead
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            TCMT IO TermHead -> MaybeT TCM TermHead
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO TermHead -> MaybeT TCM TermHead)
-> TCMT IO TermHead -> MaybeT TCM TermHead
forall a b. (a -> b) -> a -> b
$ TermHead -> Maybe TermHead -> TermHead
forall a. a -> Maybe a -> a
fromMaybe TermHead
UnknownHead (Maybe TermHead -> TermHead)
-> TCM (Maybe TermHead) -> TCMT IO TermHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              Telescope -> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) (TCM (Maybe TermHead) -> TCM (Maybe TermHead))
-> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$
                Term -> TCM (Maybe TermHead)
headSymbol Term
body
        [Map TermHead [Clause]] -> MaybeT TCM [Map TermHead [Clause]]
forall (m :: * -> *) a. Monad m => a -> m a
return [TermHead -> [Clause] -> Map TermHead [Clause]
forall k a. k -> a -> Map k a
Map.singleton TermHead
h [Clause
c]]
      computeHead Clause
_ = [Map TermHead [Clause]] -> MaybeT TCM [Map TermHead [Clause]]
forall (m :: * -> *) a. Monad m => a -> m a
return []

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

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

  VerboseKey -> VerboseLevel -> VerboseKey -> MaybeT TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
"tc.inj.check" VerboseLevel
20 (VerboseKey -> MaybeT TCM ()) -> VerboseKey -> MaybeT TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
f VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is potentially injective."
  VerboseKey -> VerboseLevel -> TCM Doc -> MaybeT TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.check" VerboseLevel
30 (TCM Doc -> MaybeT TCM ()) -> TCM Doc -> MaybeT TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
    [(TermHead, [Clause])]
-> ((TermHead, [Clause]) -> TCM Doc) -> [TCM Doc]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Map TermHead [Clause] -> [(TermHead, [Clause])]
forall k a. Map k a -> [(k, a)]
Map.toList Map TermHead [Clause]
hdMap) (((TermHead, [Clause]) -> TCM Doc) -> [TCM Doc])
-> ((TermHead, [Clause]) -> TCM Doc) -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ \ (TermHead
h, [Clause]
uc) ->
      VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (TermHead -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow TermHead
h) 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
<+>
      case [Clause]
uc of
        [Clause
c] -> [DeBruijnPattern] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([DeBruijnPattern] -> TCM Doc) -> [DeBruijnPattern] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (NAPs -> [DeBruijnPattern]) -> NAPs -> [DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
c
        [Clause]
_   -> TCM Doc
"(multiple clauses)"

  FunctionInverse -> MaybeT TCM FunctionInverse
forall (m :: * -> *) a. Monad m => a -> m a
return (FunctionInverse -> MaybeT TCM FunctionInverse)
-> FunctionInverse -> MaybeT TCM FunctionInverse
forall a b. (a -> b) -> a -> b
$ Map TermHead [Clause] -> FunctionInverse
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 :: Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
checkOverapplication Elims
es = (TermHead -> [Clause] -> m TermHead)
-> Map TermHead [Clause] -> m (Map TermHead [Clause])
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 | (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
isOverapplied) [Clause]
cs = TermHead -> m TermHead
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h
    overapplied TermHead
h [Clause]
cs = m Bool -> m TermHead -> m TermHead -> m TermHead
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TermHead -> m Bool
forall (m :: * -> *). HasConstInfo m => TermHead -> m Bool
isSuperRigid TermHead
h) (TermHead -> m TermHead
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h) (TermHead -> m TermHead
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     = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
PiHead       = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid VarHead{}    = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
UnknownHead  = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- or False, doesn't matter
    isSuperRigid (ConsHead QName
q) = do
      Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
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 DataOrRecord -> DataOrRecord -> Bool
forall a. Eq a => a -> a -> Bool
== DataOrRecord
IsData Bool -> Bool -> Bool
|| [Arg QName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Arg QName]
fs   -- Record constructors can be eliminated by projections
        Primitive{}    -> Bool
False
        PrimitiveSort{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
        GeneralizableVar{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__


    isOverapplied :: Clause -> Bool
isOverapplied Clause{ namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps } = Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
es VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> NAPs -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
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 :: QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
instantiateVarHeads QName
f Elims
es InversionMap c
m = MaybeT m (InversionMap c) -> m (Maybe (InversionMap c))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (InversionMap c) -> m (Maybe (InversionMap c)))
-> MaybeT m (InversionMap c) -> m (Maybe (InversionMap c))
forall a b. (a -> b) -> a -> b
$ (TermHead -> [c] -> MaybeT m TermHead)
-> InversionMap c -> MaybeT m (InversionMap c)
forall (m :: * -> *) c.
Monad m =>
(TermHead -> [c] -> m TermHead)
-> InversionMap c -> m (InversionMap c)
updateHeads (MaybeT m TermHead -> [c] -> MaybeT m TermHead
forall a b. a -> b -> a
const (MaybeT m TermHead -> [c] -> MaybeT m TermHead)
-> (TermHead -> MaybeT m TermHead)
-> TermHead
-> [c]
-> MaybeT m TermHead
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 VerboseLevel
i)
      | Just (Apply Arg Term
arg) <- Elims
es Elims -> VerboseLevel -> Maybe Elim
forall a. [a] -> VerboseLevel -> Maybe a
!!! VerboseLevel
i = m (Maybe TermHead) -> MaybeT m TermHead
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe TermHead) -> MaybeT m TermHead)
-> m (Maybe TermHead) -> MaybeT m TermHead
forall a b. (a -> b) -> a -> b
$ Term -> m (Maybe TermHead)
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m (Maybe TermHead)
headSymbol' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
      | Bool
otherwise = MaybeT m TermHead
forall (f :: * -> *) a. Alternative f => f a
empty   -- impossible?
    instHead TermHead
h = TermHead -> MaybeT m TermHead
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 :: Term -> m InvView
functionInverse = \case
  Def QName
f Elims
es -> do
    FunctionInverse
inv <- Definition -> FunctionInverse
defInverse (Definition -> FunctionInverse)
-> m Definition -> m FunctionInverse
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
    case FunctionInverse
inv of
      FunctionInverse
NotInjective -> InvView -> m InvView
forall (m :: * -> *) a. Monad m => a -> m a
return InvView
NoInv
      Inverse Map TermHead [Clause]
m    -> InvView
-> (Map TermHead [Clause] -> InvView)
-> Maybe (Map TermHead [Clause])
-> InvView
forall b a. b -> (a -> b) -> Maybe a -> b
maybe InvView
NoInv (QName -> Elims -> Map TermHead [Clause] -> InvView
Inv QName
f Elims
es) (Maybe (Map TermHead [Clause]) -> InvView)
-> m (Maybe (Map TermHead [Clause])) -> m InvView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map TermHead [Clause] -> m (Map TermHead [Clause]))
-> Maybe (Map TermHead [Clause])
-> m (Maybe (Map TermHead [Clause]))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
forall (m :: * -> *).
HasConstInfo m =>
Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
checkOverapplication Elims
es) (Maybe (Map TermHead [Clause])
 -> m (Maybe (Map TermHead [Clause])))
-> m (Maybe (Map TermHead [Clause]))
-> m (Maybe (Map TermHead [Clause]))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName
-> Elims
-> Map TermHead [Clause]
-> m (Maybe (Map TermHead [Clause]))
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
_ -> InvView -> m InvView
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 :: CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
useInjectivity CompareDirection
dir Blocker
blocker CompareAs
ty Term
blk Term
neu = Lens' VerboseLevel TCEnv
-> (VerboseLevel -> VerboseLevel) -> m () -> m ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' VerboseLevel TCEnv
eInjectivityDepth VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
succ (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  InvView
inv <- Term -> m InvView
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.
  VerboseLevel
nProblems <- Set ProblemId -> VerboseLevel
forall a. Set a -> VerboseLevel
Set.size (Set ProblemId -> VerboseLevel)
-> m (Set ProblemId) -> m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Set ProblemId) TCEnv -> m (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Set ProblemId) TCEnv
eActiveProblems
  VerboseLevel
injDepth  <- Lens' VerboseLevel TCEnv -> m VerboseLevel
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' VerboseLevel TCEnv
eInjectivityDepth
  let depth :: VerboseLevel
depth = VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max VerboseLevel
nProblems VerboseLevel
injDepth
  VerboseLevel
maxDepth  <- m VerboseLevel
forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
  case InvView
inv of
    InvView
NoInv            -> m ()
fallback  -- not invertible
    Inv QName
f Elims
blkArgs Map TermHead [Clause]
hdMap
      | VerboseLevel
depth VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
maxDepth -> Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (QName -> Warning
InversionDepthReached QName
f) m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
fallback
      | Bool
otherwise -> do
      VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.use" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
        VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"useInjectivity on" [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
        [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
blk, Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp, Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
neu, CompareAs -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM CompareAs
ty]
      let canReduceToSelf :: Bool
canReduceToSelf = TermHead -> Map TermHead [Clause] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (QName -> TermHead
ConsHead QName
f) Map TermHead [Clause]
hdMap Bool -> Bool -> Bool
|| TermHead -> Map TermHead [Clause] -> 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 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f', Bool -> Bool
not Bool
canReduceToSelf -> do
          Type
fTy <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.use" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
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] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"comparing application of injective function" [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
                  VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"at")
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCM Doc) -> Elims -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCM Doc) -> Elims -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
neuArgs
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"and type" 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
fTy
            ]
          [IsForced]
fs  <- QName -> m [IsForced]
forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
f
          [Polarity]
pol <- Comparison -> QName -> m [Polarity]
forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
cmp QName
f
          VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.invert.success" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCM Doc
"Successful spine comparison of", QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f]
          (Elims -> Elims -> m ()) -> Elims -> Elims -> m ()
forall a b. (a -> a -> b) -> a -> a -> b
app ([Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
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
_ -> Term -> m (Maybe TermHead)
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m (Maybe TermHead)
headSymbol' Term
neu m (Maybe TermHead) -> (Maybe TermHead -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
          Maybe TermHead
Nothing -> do
            VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.use" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
              VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"no head symbol found for" [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
neu] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
", so not inverting"
            m ()
fallback
          Just (ConsHead QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f', Bool
canReduceToSelf -> do
            VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.use" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
              VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"head symbol" [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f'] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCM Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"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 -> Comparison
-> Term
-> InvView
-> TermHead
-> m ()
-> m ()
-> (Term -> m ())
-> m ()
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 = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> TypeError) -> Term -> Term -> TypeError
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     = Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Constraint) -> Term -> Term -> Constraint
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' = (Term -> Term -> m ()) -> Term -> Term -> m ()
forall a b. (a -> a -> b) -> a -> a -> b
app (Comparison -> CompareAs -> Term -> Term -> m ()
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 :: (Comparison, (a -> a -> b) -> a -> a -> b)
cmpApp = case CompareDirection
dir of
      CompareDirection
DirEq -> (Comparison
CmpEq, (a -> a -> b) -> a -> a -> b
forall a. a -> a
id)
      CompareDirection
DirLeq -> (Comparison
CmpLeq, (a -> a -> b) -> a -> a -> b
forall a. a -> a
id)
      CompareDirection
DirGeq -> (Comparison
CmpLeq, (a -> a -> b) -> a -> a -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip)
    (Comparison
cmp, (a -> a -> b) -> a -> a -> b
app) = (Comparison, (a -> a -> b) -> a -> a -> b)
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 :: 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 (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.use" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
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
"inverting injective function" 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
hsep [QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f, TCM Doc
":", Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fTy]
      , TCM Doc
"for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TermHead -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"args =" 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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Elim -> TCM Doc) -> Elims -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs)
      ]                         -- Clauses with unknown heads are also possible candidates
    case [Clause] -> Maybe [Clause] -> [Clause]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Clause] -> [Clause]) -> Maybe [Clause] -> [Clause]
forall a b. (a -> b) -> a -> b
$ TermHead -> Map TermHead [Clause] -> Maybe [Clause]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TermHead
hd Map TermHead [Clause]
hdMap Maybe [Clause] -> Maybe [Clause] -> Maybe [Clause]
forall a. Semigroup a => a -> a -> a
<> TermHead -> Map TermHead [Clause] -> Maybe [Clause]
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 }] -> m () -> m KeepMetas -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas m ()
fallback (m KeepMetas -> m ()) -> m KeepMetas -> m ()
forall a b. (a -> b) -> a -> b
$ do
          let ps :: [Arg DeBruijnPattern]
ps   = Clause -> [Arg DeBruijnPattern]
clausePats Clause
cl
              perm :: Permutation
perm = 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
          -- These are what dot patterns should be instantiated at
          [Term]
ms <- (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] -> [Term]) -> m [Arg Term] -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m [Arg Term]
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m [Arg Term]
newTelMeta Telescope
tel
          VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.invert" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
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
"meta patterns" 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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Term -> TCM Doc) -> [Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
ms)
            , TCM Doc
"  perm =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm)
            , TCM Doc
"  tel  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
            , TCM Doc
"  ps   =" 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, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg DeBruijnPattern -> TCM Doc)
-> [Arg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Arg DeBruijnPattern -> VerboseKey)
-> Arg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg DeBruijnPattern -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [Arg DeBruijnPattern]
ps)
            ]
          -- and this is the order the variables occur in the patterns
          let msAux :: [Term]
msAux = Permutation -> [Term] -> [Term]
forall a. Permutation -> [a] -> [a]
permute (VerboseLevel -> Permutation -> Permutation
invertP VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
perm) [Term]
ms
          let sub :: Substitution' Term
sub   = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
ms)
          Elims
margs <- ReaderT (Substitution' Term) m Elims
-> Substitution' Term -> m Elims
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (StateT [Term] (ReaderT (Substitution' Term) m) Elims
-> [Term] -> ReaderT (Substitution' Term) m Elims
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((Arg DeBruijnPattern
 -> StateT [Term] (ReaderT (Substitution' Term) m) Elim)
-> [Arg DeBruijnPattern]
-> StateT [Term] (ReaderT (Substitution' Term) m) Elims
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg DeBruijnPattern
-> StateT [Term] (ReaderT (Substitution' Term) m) Elim
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
          VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.invert" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
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
"inversion"
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
"lhs  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
margs
              , TCM Doc
"rhs  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
blkArgs
              , TCM Doc
"type =" 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
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 ([Polarity] -> [Polarity]) -> m [Polarity] -> m [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison -> QName -> m [Polarity]
forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
cmp QName
f
          [IsForced]
fs  <- QName -> m [IsForced]
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' = VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
take (Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
margs) Elims
blkArgs
          [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
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) Term
r <- ReduceM (Reduced (Blocked' Term Term) Term)
-> m (Reduced (Blocked' Term Term) Term)
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Reduced (Blocked' Term Term) Term)
 -> m (Reduced (Blocked' Term Term) Term))
-> ReduceM (Reduced (Blocked' Term Term) Term)
-> m (Reduced (Blocked' Term Term) Term)
forall a b. (a -> b) -> a -> b
$ Bool
-> Term
-> QName
-> Elims
-> ReduceM (Reduced (Blocked' Term Term) Term)
unfoldDefinitionStep Bool
False (QName -> Elims -> Term
Def QName
f []) QName
f Elims
blkArgs
          case Reduced (Blocked' Term Term) Term
r of
            YesReduction Simplification
_ Term
blk' -> do
              VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.invert.success" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCM Doc
"Successful inversion of", QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f, TCM Doc
"at", TermHead -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd]
              KeepMetas
KeepMetas KeepMetas -> m () -> m KeepMetas
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> m ()
success Term
blk'
            NoReduction{}       -> do
              VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.inj.invert" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
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
"aborting inversion;" 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
blk
                , TCM Doc
"does not reduce"
                ]
              KeepMetas -> m KeepMetas
forall (m :: * -> *) a. Monad m => a -> m a
return KeepMetas
RollBackMetas
  where
    nextMeta :: (MonadState [Term] m, MonadFail m) => m Term
    nextMeta :: m Term
nextMeta = do
      Term
m : [Term]
ms <- m [Term]
forall s (m :: * -> *). MonadState s m => m s
get
      [Term] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Term]
ms
      Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
m

    dotP :: MonadReader Substitution m => Term -> m Term
    dotP :: Term -> m Term
dotP Term
v = do
      Substitution' Term
sub <- m (Substitution' Term)
forall r (m :: * -> *). MonadReader r m => m r
ask
      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
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sub Term
v

    metaElim
      :: (MonadState [Term] m, MonadReader Substitution m, HasConstInfo m, MonadFail m)
      => Arg DeBruijnPattern -> m Elim
    metaElim :: Arg DeBruijnPattern -> m Elim
metaElim (Arg ArgInfo
_ (ProjP ProjOrigin
o QName
p))  = ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o (QName -> Elim) -> m QName -> m Elim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
p
    metaElim (Arg ArgInfo
info DeBruijnPattern
p)         = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Term -> Arg Term) -> Term -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Elim) -> m Term -> m Elim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> m Term
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 :: NAPs -> m [Arg Term]
metaArgs NAPs
args = (NamedArg DeBruijnPattern -> m (Arg Term)) -> NAPs -> m [Arg Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Named NamedName DeBruijnPattern -> m Term)
-> NamedArg DeBruijnPattern -> m (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Named NamedName DeBruijnPattern -> m Term)
 -> NamedArg DeBruijnPattern -> m (Arg Term))
-> (Named NamedName DeBruijnPattern -> m Term)
-> NamedArg DeBruijnPattern
-> m (Arg Term)
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> m Term
forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
DeBruijnPattern -> m Term
metaPat (DeBruijnPattern -> m Term)
-> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> Named NamedName DeBruijnPattern
-> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) NAPs
args

    metaPat
      :: (MonadState [Term] m, MonadReader Substitution m, MonadFail m)
      => DeBruijnPattern -> m Term
    metaPat :: DeBruijnPattern -> m Term
metaPat (DotP PatternInfo
_ Term
v)       = Term -> m Term
forall (m :: * -> *).
MonadReader (Substitution' Term) m =>
Term -> m Term
dotP Term
v
    metaPat (VarP PatternInfo
_ DBPatVar
_)       = m Term
forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
nextMeta
    metaPat (IApplyP{})      = m Term
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) (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> m [Arg Term] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs -> m [Arg Term]
forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
NAPs -> m [Arg Term]
metaArgs NAPs
args
    metaPat (DefP PatternInfo
o QName
q NAPs
args)  = QName -> Elims -> Term
Def QName
q (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> m [Arg Term] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs -> m [Arg Term]
forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail m) =>
NAPs -> m [Arg Term]
metaArgs NAPs
args
    metaPat (LitP PatternInfo
_ Literal
l)       = 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
$ Literal -> Term
Lit Literal
l
    metaPat ProjP{}          = m Term
forall a. HasCallStack => a
__IMPOSSIBLE__

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