{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.IApplyConfluence where
import Prelude hiding (null, (!!))
import Control.Monad
import Control.Arrow (first,second)
import qualified Data.List as List
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal.Generic
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 qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Maybe
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
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [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 :: * -> *).
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__
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 (forall a. HasRange a => a -> Range
getRange QName
f) forall a b. (a -> b) -> a -> b
$ do
let
trhs :: Type
trhs = forall e. Arg e -> e
unArg Arg Type
t
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 a. DeBruijn a => [NamedArg (Pattern' a)] -> [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.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.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 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 =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
phi Type
trhs Term
lhs Term
body
case Term
body of
MetaV MetaId
m [Elim]
es_m' | Just [Arg Term]
es_m <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es_m' ->
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii -> do
[Closure (IPBoundary' Term)]
cs' <- do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"clTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
clTel
MetaVariable
mv <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m
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" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size mTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Sized a => a -> Int
size Telescope
mTel)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size es_m =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Sized a => a -> Int
size [Arg Term]
es_m)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
mTel forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Arg Term]
es_m) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" 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
mTel, forall a. Sized a => a -> Int
size [Arg Term]
es_m))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
mTel forall a. Ord a => a -> a -> Bool
<= forall a. Sized a => a -> Int
size [Arg Term]
es_m) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => a
__IMPOSSIBLE__
let over :: Overapplied
over = if forall a. Sized a => a -> Int
size Telescope
mTel forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Arg Term]
es_m then Overapplied
NotOverapplied else Overapplied
Overapplied
TelV Telescope
mTel1 Type
_ <- forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath (forall a. Sized a => a -> Int
size [Arg Term]
es_m) Type
ty
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mTel1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
mTel1
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
mTel1 forall t. Apply t => t -> [Arg Term] -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) forall a b. (a -> b) -> a -> b
$ do
Telescope
mTel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
clTel forall a b. (a -> b) -> a -> b
$ do
() <- forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mTel.clTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (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 (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (Map Int Bool -> Blocker -> Term -> m a)
-> (Substitution -> m a)
-> m [a]
forallFaceMaps Term
phi forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ Substitution
alpha -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mTel.clTel' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (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 (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"i0S =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
alpha
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCMT IO Doc
"es :", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
es]
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCMT IO Doc
"es_alpha :", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Substitution
alpha forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Elim]
es) ]
let
loop :: Term -> ReduceM Term
loop t :: Term
t@(Def QName
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
loop t :: Term
t@(Var Int
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
loop t :: Term
t@(Con ConHead
_ ConInfo
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
loop t :: Term
t@(MetaV MetaId
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
loop Term
t = forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
loop' :: Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es = forall t a. Blocked' t a -> a
ignoreBlocking forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> ReduceM (Blocked Term))
-> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
reduceIApply' (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. a -> Blocked' t a
notBlocked) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. a -> Blocked' t a
notBlocked forall a b. (a -> b) -> a -> b
$ Term
t) [Elim]
es)
Term
lhs <- forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> ReduceM Term
loop (QName -> [Elim] -> Term
Def QName
f (Substitution
alpha forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Elim]
es))
let
idG :: [Elim]
idG = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
clTel) forall a b. (a -> b) -> a -> b
$ (forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
mTel [])
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCMT IO Doc
"lhs :", forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
lhs]
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"cxt1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (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 (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Substitution
alpha forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
CmpEq Term
phi Type
trhs Term
lhs (MetaId -> [Elim] -> Term
MetaV MetaId
m [Elim]
idG)
forall a.
[Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) (Substitution
alpha forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Arg Term]
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" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"cxt2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (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 (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
40 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
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"eqs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Term, Term)]
eqs
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure forall a b. (a -> b) -> a -> b
$ IPBoundary
{ ipbEquations :: [(Term, Term)]
ipbEquations = [(Term, Term)]
eqs
, ipbValue :: Term
ipbValue = Substitution
sigma forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
lhs
, ipbMetaApp :: Term
ipbMetaApp = Substitution
alpha forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` MetaId -> [Elim] -> Term
MetaV MetaId
m [Elim]
es_m'
, ipbOverapplied :: Overapplied
ipbOverapplied = Overapplied
over
}
let f :: InteractionPoint -> InteractionPoint
f InteractionPoint
ip = InteractionPoint
ip { ipClause :: IPClause
ipClause = case InteractionPoint -> IPClause
ipClause InteractionPoint
ip of
ipc :: IPClause
ipc@IPClause{ipcBoundary :: IPClause -> [Closure (IPBoundary' Term)]
ipcBoundary = [Closure (IPBoundary' Term)]
b}
-> IPClause
ipc {ipcBoundary :: [Closure (IPBoundary' Term)]
ipcBoundary = [Closure (IPBoundary' Term)]
b forall a. [a] -> [a] -> [a]
++ [Closure (IPBoundary' Term)]
cs'}
ipc :: IPClause
ipc@IPNoClause{} -> IPClause
ipc}
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints (forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> v) -> k -> BiMap k v -> BiMap k v
BiMap.adjust InteractionPoint -> InteractionPoint
f InteractionId
ii)
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
unifyElims :: Args
-> Args
-> (Substitution -> [(Term,Term)] -> TCM a)
-> TCM a
unifyElims :: forall a.
[Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims [Arg Term]
vs [Arg Term]
ts Substitution -> [(Term, Term)] -> TCM a
k = do
Context
dom <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
let ([(Int, Term)]
binds' , [(Term, Term)]
eqs' ) = [Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
candidate (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Term]
vs) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Term]
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,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 b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. [a] -> [a] -> [a]
(++) (forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a. a -> [a] -> [a]
:[])) [(Int, Term)]
binds')
cod :: Context
cod = Substitution -> [Int] -> Context -> Context
codomain Substitution
s (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, Term)]
binds) Context
dom
binds :: [(Int, Term)]
binds = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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
- forall a. Sized a => a -> Int
size [Arg Term]
vs))) [(Int, Term)]
binds''
eqs :: [(Term, Term)]
eqs = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a. Subst a => Int -> a -> a
raise forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Context
dom forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size [Arg Term]
vs)) 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 => [(Int, a)] -> Substitution' a
bindS [(Int, Term)]
binds
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
s (Substitution -> [Int] -> Context -> Context
codomain Substitution
s (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, Term)]
binds)) forall a b. (a -> b) -> a -> b
$ do
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,Term)],[(Term,Term)])
candidate :: [Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
candidate (Term
i:[Term]
is) (Var Int
j []:[Term]
ts) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Int
j,Term
i)forall a. a -> [a] -> [a]
:) ([Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts)
candidate (Term
i:[Term]
is) (Term
t:[Term]
ts) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Term
i,Term
t)forall a. a -> [a] -> [a]
:) ([Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts)
candidate [] [] = ([],[])
candidate [Term]
_ [Term]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
bindS :: [(Int, a)] -> Substitution' a
bindS [(Int, a)]
binds = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Int
0..forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (-Int
1forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, a)]
binds)] 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 b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup Int
i [(Int, a)]
binds)))
codomain :: Substitution
-> [Nat]
-> Context -> Context
codomain :: Substitution -> [Int] -> Context -> Context
codomain Substitution
s [Int]
vs Context
cxt = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Int
i,ContextEntry
c) -> Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`List.notElem` [Int]
vs) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Context
cxt'
where
cxt' :: Context
cxt' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
n ContextEntry
d -> forall a. Int -> Substitution' a -> Substitution' a
dropS Int
n Substitution
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` ContextEntry
d) [Int
1..] Context
cxt
unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term,Term)] -> Constraint -> TCM a) -> TCM a
unifyElimsMeta :: forall a.
MetaId
-> [Arg Term]
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m [Arg Term]
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 :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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 :: * -> *).
(MonadFail 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 [Arg Term]
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 [Arg Term]
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 [Arg Term]
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 [Arg Term]
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 -> [Arg Term] -> 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
[Arg Term]
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) [Arg Term]
es_m
(Constraint
c,Telescope
cxt) <- forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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 [Arg Term]
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.
[Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) [Arg Term]
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)