{- |

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

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

Which functions qualify for injectivity?

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

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

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

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

-}

module Agda.TypeChecking.Injectivity where

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

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

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

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance (isIrrelevantOrPropM)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.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
  | Bool -> Bool
not ((Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
properlyMatchingClause [Clause]
cs) = 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
  | 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 (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 (f :: * -> *). Alternative f => Bool -> f ()
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, Semigroup (m Doc), 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, Semigroup (m Doc), 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, Semigroup (m Doc), 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, MonadFail 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, MonadFail m) => m Term
    nextMeta :: forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => 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 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, MonadFail m)
      => Arg DeBruijnPattern -> m Elim
    metaElim :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 HasConstInfo m, MonadFail m) =>
Arg DeBruijnPattern -> m Elim
metaElim (Arg ArgInfo
_ (ProjP ProjOrigin
o QName
p))  = 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 :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail 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,
 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 :: forall (m :: * -> *).
(MonadState [Term] m, MonadReader (Substitution' Term) m,
 MonadFail 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, 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 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 ()