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