{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.IApplyConfluence where
import Prelude hiding (null, (!!))
import Control.Monad
import Control.Monad.Except
import Data.Bifunctor (first, second)
import Data.DList (DList)
import Data.Foldable (toList)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Interaction.Options
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Maybe
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Impossible
import Agda.Utils.Functor
checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ QName
f = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> Int -> m ()
__CRASH_WHEN__ VerboseKey
"tc.cover.iapply.confluence.crash" Int
666
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Checking IApply confluence of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
f forall a b. (a -> b) -> a -> b
$ \ Definition
d -> do
case Definition -> Defn
theDef Definition
d of
Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls', funCovering :: Defn -> [Clause]
funCovering = [Clause]
cls} -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"length cls =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cls)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null [Clause]
cls Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. IApplyVars p => p -> [Int]
iApplyVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats) [Clause]
cls') forall a b. (a -> b) -> a -> b
$
forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optKeepCoveringClauses forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
f forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef
forall a b. (a -> b) -> a -> b
$ ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering (forall a b. a -> b -> a
const [])
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [Clause] -> Bool -> Call
CheckFunDefCall (forall a. HasRange a => a -> Range
getRange QName
f) QName
f [] Bool
False) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Clause]
cls forall a b. (a -> b) -> a -> b
$ QName -> Clause -> TCM ()
checkIApplyConfluence QName
f
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkIApplyConfluence :: QName -> Clause -> TCM ()
checkIApplyConfluence :: QName -> Clause -> TCM ()
checkIApplyConfluence QName
f Clause
cl = case Clause
cl of
Clause {clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
Nothing} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Clause {clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
Nothing} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Clause {namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps} | NAPs -> Bool
hasDefP NAPs
ps -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
cl :: Clause
cl@Clause { clauseTel :: Clause -> Telescope
clauseTel = Telescope
clTel
, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps
, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Just Arg Type
t
, clauseBody :: Clause -> Maybe Term
clauseBody = Just Term
body
} -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Clause -> Range
clauseLHSRange Clause
cl) forall a b. (a -> b) -> a -> b
$ do
let
trhs :: Type
trhs = forall e. Arg e -> e
unArg Arg Type
t
Maybe (Closure Call)
oldCall <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
clTel
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
ps
NAPs
ps <- forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP NAPs
ps
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall p. IApplyVars p => p -> [Int]
iApplyVars NAPs
ps) forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
let phi :: Term
phi = IntervalView -> Term
unview forall a b. (a -> b) -> a -> b
$ Arg Term -> Arg Term -> IntervalView
IMax (forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ IntervalView -> Term
unview (Arg Term -> IntervalView
INeg forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i)) forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
let es :: [Elim]
es = NAPs -> [Elim]
patternsToElims NAPs
ps
let lhs :: Term
lhs = QName -> [Elim] -> Term
Def QName
f [Elim]
es
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"clause:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
ps forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
body
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"body =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
body
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Γ =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
clTel
let
k :: Substitution -> Comparison -> Type -> Term -> Term -> TCM ()
k :: Substitution -> Comparison -> Type -> Term -> Term -> TCM ()
k Substitution
phi Comparison
cmp Type
ty Term
u Term
v | NAPs -> Bool
hasDefP NAPs
ps = forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm Comparison
cmp Type
ty Term
u Term
v
k Substitution
phi Comparison
cmp Type
ty Term
u Term
v = do
Term
u_e <- forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
u
(Doc
u_p, Doc
v_p) <- (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u_e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
v)
let
why :: Call
why = Range -> QName -> Term -> Term -> Term -> Type -> Call
CheckIApplyConfluence
(forall a. HasRange a => a -> Range
getRange Clause
cl) QName
f
(forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
phi Term
lhs)
Term
u_e Term
v Type
ty
maybeDropCall :: TCErr -> TCM ()
maybeDropCall e :: TCErr
e@(TypeError CallStack
loc TCState
s Closure TypeError
err)
| UnequalTerms Comparison
_ Term
u' Term
v' CompareAs
_ <- forall a. Closure a -> a
clValue Closure TypeError
err =
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (forall a b. a -> b -> a
const TCState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
err forall a b. (a -> b) -> a -> b
$ \TypeError
e' -> do
Doc
u' <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
u'
Doc
v' <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
v'
if (Doc
u_p forall a. Eq a => a -> a -> Bool
== Doc
u' Bool -> Bool -> Bool
&& Doc
v_p forall a. Eq a => a -> a -> Bool
== Doc
v')
then forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envCall :: Maybe (Closure Call)
envCall = Maybe (Closure Call)
oldCall }) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
e'
else forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e
maybeDropCall TCErr
x = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
x
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
why (forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm Comparison
cmp Type
ty Term
u Term
v forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCErr -> TCM ()
maybeDropCall)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
clTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
(Substitution -> Comparison -> Type -> Term -> Term -> m ())
-> Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace' Substitution -> Comparison -> Type -> Term -> Term -> TCM ()
k Comparison
CmpEq Term
phi Type
trhs Term
lhs Term
body
unifyElims :: Args
-> Args
-> (Substitution -> [(Term,Term)] -> TCM a)
-> TCM a
unifyElims :: forall a.
Args -> Args -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims Args
vs Args
ts Substitution -> [(Term, Term)] -> TCM a
k = do
Context
dom <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
let ([(Int, DList Term)]
binds' , [(Term, Term)]
eqs' ) = [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
ts)
([(Int, Term)]
binds'', [[(Term, Term)]]
eqss') =
forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
j, DList Term
tts) -> case forall (t :: * -> *) a. Foldable t => t a -> [a]
toList DList Term
tts of
Term
t : [Term]
ts -> ((Int
j, Term
t), forall a b. (a -> b) -> [a] -> [b]
map (, Int -> Term
var Int
j) [Term]
ts)
[] -> forall a. HasCallStack => a
__IMPOSSIBLE__) forall a b. (a -> b) -> a -> b
$
forall a. IntMap a -> [(Int, a)]
IntMap.toList forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMap.fromListWith forall a. Semigroup a => a -> a -> a
(<>) [(Int, DList Term)]
binds'
cod' :: Context -> Context
cod' = Substitution -> IntSet -> Context -> Context
codomain Substitution
s ([Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, Term)]
binds'')
cod :: Context
cod = Context -> Context
cod' Context
dom
svs :: Int
svs = forall a. Sized a => a -> Int
size Args
vs
binds :: IntMap Term
binds = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Context
cod forall a. Num a => a -> a -> a
- Int
svs))) [(Int, Term)]
binds''
eqs :: [(Term, Term)]
eqs = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Context
dom forall a. Num a => a -> a -> a
- Int
svs))) forall a b. (a -> b) -> a -> b
$
[(Term, Term)]
eqs' forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Term, Term)]]
eqss'
s :: Substitution
s = forall {a}. DeBruijn a => IntMap a -> Substitution' a
bindS IntMap Term
binds
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
s Context -> Context
cod' forall a b. (a -> b) -> a -> b
$ Substitution -> [(Term, Term)] -> TCM a
k Substitution
s (Substitution
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [(Term, Term)]
eqs)
where
candidate :: [Term] -> [Term] -> ([(Nat, DList Term)], [(Term, Term)])
candidate :: [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts = case ([Term]
is, [Term]
ts) of
(Term
i : [Term]
is, Var Int
j [] : [Term]
ts) -> forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Int
j, forall el coll. Singleton el coll => el -> coll
singleton Term
i) forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
[Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts
(Term
i : [Term]
is, Term
t : [Term]
ts) -> forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Term
i, Term
t) forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
[Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts
([], []) -> ([], [])
([Term], [Term])
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
bindS :: IntMap a -> Substitution' a
bindS IntMap a
binds = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$
case forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMax IntMap a
binds of
Maybe (Int, a)
Nothing -> []
Just (Int
max, a
_) -> forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Int
0 .. Int
max] forall a b. (a -> b) -> a -> b
$ \Int
i ->
forall a. a -> Maybe a -> a
fromMaybe (forall a. DeBruijn a => Int -> a
deBruijnVar Int
i) (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap a
binds)
codomain
:: Substitution
-> IntSet
-> Context -> Context
codomain :: Substitution -> IntSet -> Context -> Context
codomain Substitution
s IntSet
vs =
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Int
i, ContextEntry
c) -> if Int
i Int -> IntSet -> Bool
`IntSet.member` IntSet
vs
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just ContextEntry
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i ContextEntry
c -> (Int
i, forall a. Int -> Substitution' a -> Substitution' a
dropS (Int
i forall a. Num a => a -> a -> a
+ Int
1) Substitution
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` ContextEntry
c)) [Int
0..]
unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term,Term)] -> Constraint -> TCM a) -> TCM a
unifyElimsMeta :: forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
es_m Closure Constraint
cl [(Term, Term)] -> Constraint -> TCM a
k = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Constraint -> TCM a
k []) forall a b. (a -> b) -> a -> b
$ do
MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do
Type
ty <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
m
Telescope
mTel0 <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
mTel0 forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Args
es_m) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"funny number of elims" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show (forall a. Sized a => a -> Int
size Telescope
mTel0, forall a. Sized a => a -> Int
size Args
es_m))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
mTel0 forall a. Ord a => a -> a -> Bool
<= forall a. Sized a => a -> Int
size Args
es_m) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ty: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty
TelV Telescope
mTel1 Type
_ <- forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath (forall a. Sized a => a -> Int
size Args
es_m) Type
ty
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
mTel1 forall t. Apply t => t -> Args -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel0) forall a b. (a -> b) -> a -> b
$ do
Telescope
mTel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mTel: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
mTel
Args
es_m <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall a. Sized a => a -> Int
size Telescope
mTel) Args
es_m
(Constraint
c,Telescope
cxt) <- forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl forall a b. (a -> b) -> a -> b
$ \ Constraint
c -> (Constraint
c,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
cxt
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
cxt forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"es_m" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
es_m
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying unifyElims"
forall a.
Args -> Args -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) Args
es_m forall a b. (a -> b) -> a -> b
$ \ Substitution
sigma [(Term, Term)]
eqs -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"gotten a substitution"
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sigma:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
sigma
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sigma:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
sigma
[(Term, Term)] -> Constraint -> TCM a
k [(Term, Term)]
eqs (Substitution
sigma forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Constraint
c)