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
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
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."
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__
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) $
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)
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
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
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
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
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__
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
(<>)
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
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
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
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
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 []
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
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
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
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)
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
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
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
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
instHead TermHead
h = TermHead -> MaybeT m TermHead
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return TermHead
h
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)
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
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
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
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
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
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
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
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)
]
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
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)
]
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
]
]
pol <- purgeNonvariant <$> getPolarity' cmp f
fs <- getForcedArgs f
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'
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, MonadFail m) => m Term
nextMeta :: forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
nextMeta = do
m : ms <- m [Term]
forall s (m :: * -> *). MonadState s m => m s
get
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, 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
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 ()