{- |

"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       ( MonadError )
import Control.Monad.State        ( evalStateT, MonadState, gets, put )
import Control.Monad.Reader       ( runReaderT, MonadReader, ask )
import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )

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.Patterns.Match (properlyMatching')
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope.Path
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.Syntax.Common.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 <- 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 a. a -> TCMT IO a
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 a. a -> TCMT IO 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
          [Char] -> Nat -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.axiom" Nat
50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"headSymbol: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f [Char] -> [Char] -> [Char]
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).
          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
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm 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
$ do
                 QName
q <- QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
                 TCMT IO Bool
-> TCM (Maybe TermHead)
-> TCM (Maybe TermHead)
-> TCM (Maybe TermHead)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
q) (Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing) (TCM (Maybe TermHead) -> TCM (Maybe TermHead))
-> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$
                     {- else -}     Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
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
q
    Sort Sort
_  -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just TermHead
PiHead)
    Var Nat
i [] -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
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
$ Nat -> TermHead
VarHead Nat
i) -- Only naked variables. Otherwise substituting a neutral term is not guaranteed to stay neutral.
    Lit Literal
_   -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    Var{}   -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    Level{} -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    MetaV{} -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    DontCare{} -> Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
    Dummy [Char]
s Elims
_ -> [Char] -> TCM (Maybe TermHead)
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 <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
  [Maybe QName]
prims <- (PrimitiveId -> m (Maybe QName))
-> [PrimitiveId] -> m [Maybe QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName'
    [ PrimitiveId
builtinHComp
    , PrimitiveId
builtinComp
    , PrimitiveId
builtinTrans
    , PrimitiveId
builtinGlue
    , PrimitiveId
builtin_glue
    , PrimitiveId
builtin_glueU ]
  case Definition -> Defn
theDef Definition
defn of
    Defn
_ | (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qn) Maybe QName -> [Maybe QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
prims -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Function{funIsKanOp :: Defn -> Maybe QName
funIsKanOp = Just QName
_} -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Defn
_ -> Bool -> m Bool
forall a. a -> m a
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 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' Term a -> f (Blocked' Term 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 a. a -> m a
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
_    ->
        m Bool
-> m (Maybe TermHead) -> m (Maybe TermHead) -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). PureTCM m => QName -> m Bool
isUnstableDef QName
g)
          (Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TermHead
forall a. Maybe a
Nothing)
          (Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe TermHead -> m (Maybe TermHead))
-> (TermHead -> Maybe TermHead) -> TermHead -> m (Maybe TermHead)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (TermHead -> m (Maybe TermHead)) -> TermHead -> m (Maybe TermHead)
forall a b. (a -> b) -> a -> b
$ QName -> TermHead
ConsHead QName
g)
      Con ConHead
c ConInfo
_ Elims
_  -> do
        QName
q <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
        m Bool
-> m (Maybe TermHead) -> m (Maybe TermHead) -> m (Maybe TermHead)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
q)
          (Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TermHead
forall a. Maybe a
Nothing)
          (Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
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
q)
      Var Nat
i Elims
_    -> Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
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 (Nat -> TermHead
VarHead Nat
i)
      Sort Sort
_     -> Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      Lam{}      -> Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      Level{}    -> Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TermHead
forall a. Maybe a
Nothing
      DontCare{} -> Maybe TermHead -> m (Maybe TermHead)
forall a. a -> m a
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 [Char]
s Elims
_  -> [Char] -> m (Maybe TermHead)
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)) <- [Nat] -> [DeBruijnPattern] -> [(Nat, DeBruijnPattern)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
0..] ([DeBruijnPattern] -> [(Nat, DeBruijnPattern)])
-> [DeBruijnPattern] -> [(Nat, 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, Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j ] of
    []    -> Maybe TermHead
forall a. Maybe a
Nothing
    [Nat
n]   -> TermHead -> Maybe TermHead
forall a. a -> Maybe a
Just (Nat -> TermHead
VarHead Nat
n)
    Nat
_:Nat
_:[Nat]
_ -> Maybe TermHead
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Join a list of inversion maps.
joinHeadMaps :: [InversionMap c] -> InversionMap c
joinHeadMaps :: forall c. [InversionMap c] -> InversionMap c
joinHeadMaps = ([c] -> [c] -> [c]) -> [Map TermHead [c]] -> Map TermHead [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 :: forall (m :: * -> *) c.
Monad m =>
(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 = do
    TCMT IO Bool
-> TCM FunctionInverse
-> TCM FunctionInverse
-> TCM FunctionInverse
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Clause -> TCMT IO Bool) -> [Clause] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
anyM Clause -> TCMT IO Bool
properlyMatchingClause [Clause]
cs) {-then-} (QName -> [Clause] -> TCM FunctionInverse
checkInjectivity' QName
f [Clause]
cs) {-else-} do
      [Char] -> Nat -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check.pointless" Nat
35 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [Char]
"Injectivity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> QName
A.qnameToConcrete QName
f) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" would be pointless."
      FunctionInverse -> TCM FunctionInverse
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunctionInverse
forall c. FunctionInverse' c
NotInjective
  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 -> TCMT IO Bool
properlyMatchingClause =
      (NamedArg DeBruijnPattern -> TCMT IO Bool) -> NAPs -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
anyM (Bool -> Bool -> DeBruijnPattern -> TCMT IO Bool
forall (m :: * -> *) a.
HasConstInfo m =>
Bool -> Bool -> Pattern' a -> m Bool
properlyMatching' Bool
False Bool
False (DeBruijnPattern -> TCMT IO Bool)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) (NAPs -> TCMT IO Bool)
-> (Clause -> NAPs) -> Clause -> TCMT IO 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 (TCMT IO) FunctionInverse
    -> TCMT IO (Maybe FunctionInverse))
-> MaybeT (TCMT IO) FunctionInverse
-> TCM FunctionInverse
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MaybeT (TCMT IO) FunctionInverse -> TCMT IO (Maybe FunctionInverse)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) FunctionInverse -> TCM FunctionInverse)
-> MaybeT (TCMT IO) FunctionInverse -> TCM FunctionInverse
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Nat -> [Char] -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Nat
40 ([Char] -> MaybeT (TCMT IO) ()) -> [Char] -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking injectivity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
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) = TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead)
-> TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead
forall a b. (a -> b) -> a -> b
$ Maybe TermHead -> TCM (Maybe TermHead)
forall a. a -> TCMT IO a
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 -> Nat -> Maybe TermHead
topLevelArg Clause
c Nat
i
      varToArg Clause
_ TermHead
h           = TermHead -> MaybeT (TCMT IO) TermHead
forall a. a -> MaybeT (TCMT IO) a
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) = [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
forall a. a -> MaybeT (TCMT IO) a
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 } = Telescope
-> MaybeT (TCMT IO) [Map TermHead [Clause]]
-> MaybeT (TCMT IO) [Map TermHead [Clause]]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) (MaybeT (TCMT IO) [Map TermHead [Clause]]
 -> MaybeT (TCMT IO) [Map TermHead [Clause]])
-> MaybeT (TCMT IO) [Map TermHead [Clause]]
-> MaybeT (TCMT IO) [Map TermHead [Clause]]
forall a b. (a -> b) -> a -> b
$ 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 (TCMT IO)) Bool
    -> MaybeT (TCMT IO) (Either Blocker Bool))
-> BlockT (MaybeT (TCMT IO)) Bool
-> MaybeT (TCMT IO) Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BlockT (MaybeT (TCMT IO)) Bool
-> MaybeT (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (MaybeT (TCMT IO)) Bool -> MaybeT (TCMT IO) Bool)
-> BlockT (MaybeT (TCMT IO)) Bool -> MaybeT (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ Arg Type -> BlockT (MaybeT (TCMT IO)) Bool
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 = NAPs -> [Nat]
forall p. IApplyVars p => p -> [Nat]
iApplyVars (Clause -> NAPs
namedClausePats Clause
c)
        Bool -> MaybeT (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard ([Nat] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
ivars)
        TermHead
h <- if Bool
maybeIrr then TermHead -> MaybeT (TCMT IO) TermHead
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
UnknownHead else
          Clause -> TermHead -> MaybeT (TCMT IO) TermHead
varToArg Clause
c (TermHead -> MaybeT (TCMT IO) TermHead)
-> MaybeT (TCMT IO) TermHead -> MaybeT (TCMT IO) TermHead
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            TCM TermHead -> MaybeT (TCMT IO) TermHead
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM TermHead -> MaybeT (TCMT IO) TermHead)
-> TCM TermHead -> MaybeT (TCMT IO) 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) -> TCM TermHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              Term -> TCM (Maybe TermHead)
headSymbol Term
body
        [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
forall a. a -> MaybeT (TCMT IO) a
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 (TCMT IO) [Map TermHead [Clause]]
forall a. a -> MaybeT (TCMT IO) a
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 (TCMT IO) [[Map TermHead [Clause]]]
-> MaybeT (TCMT IO) (Map TermHead [Clause])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]])
-> [Clause] -> MaybeT (TCMT IO) [[Map TermHead [Clause]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Clause -> MaybeT (TCMT IO) [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 (TCMT IO) ()
forall a. MaybeT (TCMT IO) a
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 (TCMT IO) ()
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  [Char] -> Nat -> [Char] -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn  [Char]
"tc.inj.check" Nat
20 ([Char] -> MaybeT (TCMT IO) ()) -> [Char] -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is potentially injective."
  [Char] -> Nat -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.check" Nat
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    [(TermHead, [Clause])]
-> ((TermHead, [Clause]) -> TCMT IO Doc) -> [TCMT IO 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]) -> TCMT IO Doc) -> [TCMT IO Doc])
-> ((TermHead, [Clause]) -> TCMT IO Doc) -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ \ (TermHead
h, [Clause]
uc) ->
      [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (TermHead -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TermHead
h) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      case [Clause]
uc of
        [Clause
c] -> [DeBruijnPattern] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
prettyTCM ([DeBruijnPattern] -> TCMT IO Doc)
-> [DeBruijnPattern] -> TCMT IO 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]
_   -> TCMT IO Doc
"(multiple clauses)"
  FunctionInverse -> MaybeT (TCMT IO) FunctionInverse
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunctionInverse -> MaybeT (TCMT IO) FunctionInverse)
-> FunctionInverse -> MaybeT (TCMT IO) 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 :: forall (m :: * -> *).
HasConstInfo m =>
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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h) (TermHead -> m TermHead
forall a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
PiHead       = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid VarHead{}    = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    isSuperRigid TermHead
UnknownHead  = Bool -> m Bool
forall a. a -> m a
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 a. a -> m a
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
forall p. DataOrRecord' p
IsData Bool -> Bool -> Bool
|| [Arg QName] -> Bool
forall a. [a] -> 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 -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> NAPs -> Nat
forall a. [a] -> Nat
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 = 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 Nat
i)
      | Just (Apply Arg Term
arg) <- Elims
es Elims -> Nat -> Maybe Elim
forall a. [a] -> Nat -> Maybe a
!!! Nat
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 a. MaybeT m a
forall (f :: * -> *) a. Alternative f => f a
empty   -- impossible?
    instHead TermHead
h = TermHead -> MaybeT m TermHead
forall a. a -> MaybeT m a
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 (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
    Maybe Cubical
cubical <- m (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
    case FunctionInverse
inv of
      FunctionInverse
NotInjective -> InvView -> m InvView
forall a. a -> m a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe 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 a. a -> m a
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 = Lens' TCEnv Nat -> (Nat -> Nat) -> m () -> m ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Nat -> f Nat) -> TCEnv -> f TCEnv
Lens' TCEnv Nat
eInjectivityDepth Nat -> Nat
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.
  Nat
nProblems <- Set ProblemId -> Nat
forall a. Set a -> Nat
Set.size (Set ProblemId -> Nat) -> m (Set ProblemId) -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv (Set ProblemId) -> m (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  Nat
injDepth  <- Lens' TCEnv Nat -> m Nat
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Nat -> f Nat) -> TCEnv -> f TCEnv
Lens' TCEnv Nat
eInjectivityDepth
  let depth :: Nat
depth = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
nProblems Nat
injDepth
  Nat
maxDepth  <- m Nat
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 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
maxDepth -> Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (QName -> Warning
InversionDepthReached QName
f) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
fallback
      | Bool
otherwise -> do
      [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"useInjectivity on" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
        [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
blk, Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
neu, CompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM CompareAs
ty]
      ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"compare by reduction: injectivity"
      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
          [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"comparing application of injective function" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
                  [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"at")
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elims
blkArgs
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elims
neuArgs
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"and type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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
          [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert.success" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"Successful spine comparison of", QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f]
          ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"compare by reduction: injectivity successful"
          (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 a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
          Maybe TermHead
Nothing -> do
            [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"no head symbol found for" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
neu] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
", 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
            [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"head symbol" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f'] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [TCMT IO Doc]
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 -> 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 :: forall a b. (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 :: 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 (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
    [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.use" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"inverting injective function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f, TCMT IO Doc
":", Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
fTy]
      , TCMT IO Doc
"for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TermHead -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd
      , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> 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
          [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"meta patterns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM [Term]
ms)
            , TCMT IO Doc
"  perm =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
            , TCMT IO Doc
"  tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
            , TCMT IO Doc
"  ps   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg DeBruijnPattern -> TCMT IO Doc)
-> [Arg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Arg DeBruijnPattern -> [Char])
-> Arg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg DeBruijnPattern -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [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 (Nat -> Permutation -> Permutation
invertP Nat
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Arg DeBruijnPattern
-> StateT [Term] (ReaderT (Substitution' Term) m) Elim
forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 HasConstInfo m) =>
Arg DeBruijnPattern -> m Elim
metaElim [Arg DeBruijnPattern]
ps) [Term]
msAux) Substitution' Term
sub
          [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"inversion"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"lhs  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
margs
              , TCMT IO Doc
"rhs  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
blkArgs
              , TCMT IO Doc
"type =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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' = Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
take (Elims -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
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 a. ReduceM a -> m a
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
$ Term
-> QName -> Elims -> ReduceM (Reduced (Blocked' Term Term) Term)
unfoldDefinitionStep (QName -> Elims -> Term
Def QName
f []) QName
f Elims
blkArgs
          case Reduced (Blocked' Term Term) Term
r of
            YesReduction Simplification
_ Term
blk' -> do
              [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert.success" Nat
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"Successful inversion of", QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f, TCMT IO Doc
"at", TermHead -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TermHead
hd]
              KeepMetas
KeepMetas KeepMetas -> m () -> m KeepMetas
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> m ()
success Term
blk'
            NoReduction{}       -> do
              [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.inj.invert" Nat
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ TCMT IO Doc
"aborting inversion;" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
blk
                , TCMT IO Doc
"does not reduce"
                ]
              KeepMetas -> m KeepMetas
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return KeepMetas
RollBackMetas
  where
    nextMeta :: (MonadState [Term] m) => m Term
    nextMeta :: forall (m :: * -> *). MonadState [Term] m => m Term
nextMeta = do
      (Term
m, [Term]
ms) <- ([Term] -> (Term, [Term])) -> m (Term, [Term])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Term, [Term]) -> Maybe (Term, [Term]) -> (Term, [Term])
forall a. a -> Maybe a -> a
fromMaybe (Term, [Term])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Term, [Term]) -> (Term, [Term]))
-> ([Term] -> Maybe (Term, [Term])) -> [Term] -> (Term, [Term])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Maybe (Term, [Term])
forall a. [a] -> Maybe (a, [a])
uncons)
      [Term] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Term]
ms
      Term -> m Term
forall a. a -> m a
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 <- m (Substitution' Term)
forall r (m :: * -> *). MonadReader r m => m r
ask
      Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ 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)
      => Arg DeBruijnPattern -> m Elim
    metaElim :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 HasConstInfo m) =>
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) =>
DeBruijnPattern -> m Term
metaPat DeBruijnPattern
p

    metaArgs
      :: (MonadState [Term] m, MonadReader Substitution m)
      => [NamedArg DeBruijnPattern] -> m Args
    metaArgs :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m) =>
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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) =>
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)
      => DeBruijnPattern -> m Term
    metaPat :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m) =>
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 => m Term
nextMeta
    metaPat (IApplyP{})      = m Term
forall (m :: * -> *). MonadState [Term] 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) =>
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) =>
NAPs -> m [Arg Term]
metaArgs NAPs
args
    metaPat (LitP PatternInfo
_ Literal
l)       = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ 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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
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 a b. a -> TCMT IO b -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
  where
    fallback :: TCMT IO ()
fallback  = () -> TCMT IO ()
forall a. a -> TCMT IO a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()