{- |

"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.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

  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 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
      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 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
            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 Set.member f fs then no else 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
                 q <- QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
                 ifM (isPathCons q) (return Nothing) $
                     {- else -}     return $ Just $ ConsHead 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
  defn <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
  prims <- traverse getPrimitiveName'
    [ builtinHComp
    , builtinComp
    , builtinTrans
    , builtinGlue
    , builtin_glue
    , builtin_glueU ]
  case theDef 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
  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 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
        q <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName (ConHead -> QName
conName ConHead
c)
        ifM (isPathCons q)
          (pure Nothing)
          (return $ Just $ ConsHead 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
        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 = NAPs -> [Nat]
forall p. IApplyVars p => p -> [Nat]
iApplyVars (Clause -> NAPs
namedClausePats Clause
c)
        guard (null ivars)
        h <- if maybeIrr then return UnknownHead else
          varToArg c =<< do
            lift $ fromMaybe UnknownHead <$> do
              headSymbol body
        return [Map.singleton h [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 []

  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 Map.lookup UnknownHead 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 ()

  reportSLn  "tc.inj.check" 20 $ prettyShow f ++ " is potentially injective."
  reportSDoc "tc.inj.check" 30 $ nest 2 $ vcat $
    for (Map.toList hdMap) $ \ (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)"
  return $ Inverse 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
      def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      return $ case theDef 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
    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
    cubical <- cubicalOption
    case 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
  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.
  nProblems <- Set.size <$> viewTC eActiveProblems
  injDepth  <- viewTC eInjectivityDepth
  let depth = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
nProblems Nat
injDepth
  maxDepth  <- maxInversionDepth
  case 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
          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
          reportSDoc "tc.inj.use" 20 $ vcat
            [ fsep (pwords "comparing application of injective function" ++ [prettyTCM f] ++
                  pwords "at")
            , nest 2 $ fsep $ punctuate comma $ map prettyTCM blkArgs
            , nest 2 $ fsep $ punctuate comma $ map prettyTCM neuArgs
            , nest 2 $ "and type" <+> prettyTCM fTy
            ]
          fs  <- getForcedArgs f
          pol <- getPolarity' cmp f
          reportSDoc "tc.inj.invert.success" 20 $ hsep ["Successful spine comparison of", prettyTCM f]
          whenProfile Profile.Conversion $ tick "compare by reduction: injectivity successful"
          app (compareElims pol fs fTy (Def f [])) blkArgs 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
    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
    reportSDoc "tc.inj.use" 20 $ vcat
      [ "inverting injective function" <?> hsep [prettyTCM f, ":", prettyTCM fTy]
      , "for" <?> pretty hd
      , nest 2 $ "args =" <+> prettyList (map prettyTCM blkArgs)
      ]                         -- Clauses with unknown heads are also possible candidates
    case fromMaybe [] $ Map.lookup hd hdMap <> Map.lookup UnknownHead 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
          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
          reportSDoc "tc.inj.invert" 20 $ vcat
            [ "meta patterns" <+> prettyList (map prettyTCM ms)
            , "  perm =" <+> text (show perm)
            , "  tel  =" <+> prettyTCM tel
            , "  ps   =" <+> prettyList (map (text . prettyShow) ps)
            ]
          -- and this is the order the variables occur in the patterns
          let 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   = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
ms)
          margs <- runReaderT (evalStateT (mapM metaElim ps) msAux) sub
          reportSDoc "tc.inj.invert" 20 $ vcat
            [ "inversion"
            , nest 2 $ vcat
              [ "lhs  =" <+> prettyTCM margs
              , "rhs  =" <+> prettyTCM blkArgs
              , "type =" <+> prettyTCM 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.
          pol <- purgeNonvariant <$> getPolarity' cmp f
          fs  <- getForcedArgs f
          -- The clause might not give as many patterns as there
          -- are arguments (point-free style definitions).
          let 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
          compareElims pol fs fTy (Def f []) margs blkArgs'

          -- Check that we made progress.
          r <- liftReduce $ unfoldDefinitionStep (Def f []) f blkArgs
          case 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
      (m, 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)
      put ms
      return m

    dotP :: MonadReader Substitution m => Term -> m Term
    dotP :: forall (m :: * -> *).
MonadReader (Substitution' Term) m =>
Term -> m Term
dotP Term
v = do
      sub <- m (Substitution' Term)
forall r (m :: * -> *). MonadReader r m => m r
ask
      return $ applySubst sub 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
      inv <- Term -> TCMT IO InvView
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Term -> m InvView
functionInverse Term
blk
      blkTy <$ invertFunction CmpEq blk inv PiHead fallback err 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 ()