{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}

{-| Functions for building the left inverse part of a 'UnifyEquiv'.
 -}

module Agda.TypeChecking.Rules.LHS.Unify.LeftInverse where

import Prelude hiding ((!!), null)

import Control.Monad
import Control.Monad.State
import Control.Monad.Except

import Data.Functor

import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Names
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Records

import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Unify.Types

import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size

import Agda.Utils.Impossible


data DigestedUnifyStep
  = DSolution Int (Dom Type) (FlexibleVar Int) Term (Either () ())
  | DEtaExpandVar (FlexibleVar Int) QName Args

instance PrettyTCM DigestedUnifyStep where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DigestedUnifyStep -> m Doc
prettyTCM (DSolution Int
a Dom Type
b FlexibleVar Int
c Term
d Either () ()
e) = UnifyStep -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM (Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
a Dom Type
b FlexibleVar Int
c Term
d Either () ()
e)
  prettyTCM (DEtaExpandVar FlexibleVar Int
a QName
b [Arg Term]
c) = UnifyStep -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM (FlexibleVar Int -> QName -> [Arg Term] -> UnifyStep
EtaExpandVar FlexibleVar Int
a QName
b [Arg Term]
c)

data DigestedUnifyLogEntry
  = DUnificationStep UnifyState DigestedUnifyStep UnifyOutput

type DigestedUnifyLog = [(DigestedUnifyLogEntry,UnifyState)]

-- | Pre-process a UnifyLog so that we catch unsupported steps early.
digestUnifyLog :: UnifyLog -> Either NoLeftInv DigestedUnifyLog
digestUnifyLog :: UnifyLog -> Either NoLeftInv DigestedUnifyLog
digestUnifyLog UnifyLog
log = UnifyLog
-> ((UnifyLogEntry, UnifyState)
    -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState))
-> Either NoLeftInv DigestedUnifyLog
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM UnifyLog
log \(UnificationStep UnifyState
s UnifyStep
step UnifyOutput
out, UnifyState
s') -> do
  let illegal :: Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
illegal     = NoLeftInv -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. a -> Either a b
Left (NoLeftInv -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState))
-> NoLeftInv
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyStep -> NoLeftInv
Illegal UnifyStep
step
      unsupported :: Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
unsupported = NoLeftInv -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. a -> Either a b
Left (NoLeftInv -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState))
-> NoLeftInv
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyStep -> NoLeftInv
UnsupportedYet UnifyStep
step
      ret :: DigestedUnifyStep
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
ret DigestedUnifyStep
step    = (DigestedUnifyLogEntry, UnifyState)
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a. a -> Either NoLeftInv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UnifyState
-> DigestedUnifyStep -> UnifyOutput -> DigestedUnifyLogEntry
DUnificationStep UnifyState
s DigestedUnifyStep
step UnifyOutput
out, UnifyState
s')
  case UnifyStep
step of
    Solution Int
a Dom Type
b FlexibleVar Int
c Term
d Either () ()
e   -> DigestedUnifyStep
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
ret (DigestedUnifyStep
 -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState))
-> DigestedUnifyStep
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. (a -> b) -> a -> b
$ Int
-> Dom Type
-> FlexibleVar Int
-> Term
-> Either () ()
-> DigestedUnifyStep
DSolution Int
a Dom Type
b FlexibleVar Int
c Term
d Either () ()
e
    EtaExpandVar FlexibleVar Int
a QName
b [Arg Term]
c   -> DigestedUnifyStep
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
ret (DigestedUnifyStep
 -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState))
-> DigestedUnifyStep
-> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a b. (a -> b) -> a -> b
$ FlexibleVar Int -> QName -> [Arg Term] -> DigestedUnifyStep
DEtaExpandVar FlexibleVar Int
a QName
b [Arg Term]
c
    Deletion{}           -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
illegal
    TypeConInjectivity{} -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
illegal
    -- These should end up in a NoUnify
    Conflict{}    -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__
    LitConflict{} -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Cycle{}       -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__
    UnifyStep
_             -> Either NoLeftInv (DigestedUnifyLogEntry, UnifyState)
unsupported

instance PrettyTCM NoLeftInv where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NoLeftInv -> m Doc
prettyTCM (UnsupportedYet UnifyStep
s) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It relies on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [UnifyStep -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
explainStep UnifyStep
s m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is not yet supported"
  prettyTCM NoLeftInv
UnsupportedCxt     = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"it relies on higher-dimensional unification, which is not yet supported"
  prettyTCM (Illegal UnifyStep
s)        = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It relies on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [UnifyStep -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
explainStep UnifyStep
s m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is incompatible with" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cubical Agda"]
  prettyTCM NoLeftInv
NoCubical          = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Cubical Agda is disabled"
  prettyTCM NoLeftInv
WithKEnabled       = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"The K rule is enabled"
  prettyTCM NoLeftInv
SplitOnStrict      = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"It splits on a type in SSet"
  prettyTCM NoLeftInv
SplitOnFlat        = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"It splits on a @♭ argument"
  prettyTCM (CantTransport Closure (Abs Type)
t)  = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Closure (Abs Type) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure (Abs Type) -> m Doc
prettyTCM Closure (Abs Type)
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can not be transported"
  prettyTCM (CantTransport' Closure Type
t) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Closure Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure Type -> m Doc
prettyTCM Closure Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can not be transported"

data NoLeftInv
  = UnsupportedYet {NoLeftInv -> UnifyStep
badStep :: UnifyStep}
  | Illegal        {badStep :: UnifyStep}
  | NoCubical
  | WithKEnabled
  | SplitOnStrict  -- ^ splitting on a Strict Set.
  | SplitOnFlat    -- ^ splitting on a @♭ argument
  | UnsupportedCxt
  | CantTransport  (Closure (Abs Type))
  | CantTransport' (Closure Type)
  deriving Int -> NoLeftInv -> ShowS
[NoLeftInv] -> ShowS
NoLeftInv -> [Char]
(Int -> NoLeftInv -> ShowS)
-> (NoLeftInv -> [Char])
-> ([NoLeftInv] -> ShowS)
-> Show NoLeftInv
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoLeftInv -> ShowS
showsPrec :: Int -> NoLeftInv -> ShowS
$cshow :: NoLeftInv -> [Char]
show :: NoLeftInv -> [Char]
$cshowList :: [NoLeftInv] -> ShowS
showList :: [NoLeftInv] -> ShowS
Show

-- | Build the left inverse part of a 'UnifyEquiv' (@τ@, @leftInv@).
buildLeftInverse :: UnifyState -> UnifyLog -> TCM (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse :: UnifyState
-> UnifyLog
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
buildLeftInverse UnifyState
s0 UnifyLog
log = Account (BenchPhase (TCMT IO))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.UnifyIndices, BenchPhase (TCMT IO)
Phase
Bench.CubicalLeftInversion] (TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
 -> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term)))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a b. (a -> b) -> a -> b
$ case UnifyLog -> Either NoLeftInv DigestedUnifyLog
digestUnifyLog UnifyLog
log of
  Left NoLeftInv
no -> do
    [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv.badstep" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"No Left Inverse:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM (NoLeftInv -> UnifyStep
badStep NoLeftInv
no)
    Either NoLeftInv (Substitution' Term, Substitution' Term)
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv
-> Either NoLeftInv (Substitution' Term, Substitution' Term)
forall a b. a -> Either a b
Left NoLeftInv
no)
  Right DigestedUnifyLog
log -> do

    [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv.badstep" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
      "cubical:" <+> text (show cubical)
    [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv.badstep" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      pathp <- BuiltinId -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' BuiltinId
builtinPathP
      "pathp:" <+> text (show $ isJust pathp)
    let
      cond :: TCMT IO Bool
cond = [TCMT IO Bool] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM
        -- TODO: handle open contexts: they happen during "higher dimensional" unification,
        --       in injectivity cases.
        [ Context -> Bool
forall a. Null a => a -> Bool
null (Context -> Bool) -> TCMT IO Context -> TCMT IO Bool
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        ]

      compose :: [(Retract, Term)] -> ExceptT NoLeftInv TCM Retract
      compose :: [(Retract, Term)] -> ExceptT NoLeftInv (TCMT IO) Retract
compose [] = ExceptT NoLeftInv (TCMT IO) Retract
forall a. HasCallStack => a
__IMPOSSIBLE__
      compose [(Retract
xs, Term
_)] = Retract -> ExceptT NoLeftInv (TCMT IO) Retract
forall a. a -> ExceptT NoLeftInv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Retract
xs
      compose ((Retract
x, Term
t):[(Retract, Term)]
xs) = do
        r <- [(Retract, Term)] -> ExceptT NoLeftInv (TCMT IO) Retract
compose [(Retract, Term)]
xs
        ExceptT $ composeRetract x t r <&> \case
          Left Closure (Abs Type)
e  -> NoLeftInv -> Either NoLeftInv Retract
forall a b. a -> Either a b
Left (Closure (Abs Type) -> NoLeftInv
CantTransport Closure (Abs Type)
e)
          Right Retract
x -> Retract -> Either NoLeftInv Retract
forall a b. b -> Either a b
Right Retract
x

    TCMT IO Bool
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
cond (Either NoLeftInv (Substitution' Term, Substitution' Term)
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NoLeftInv (Substitution' Term, Substitution' Term)
 -> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term)))
-> Either NoLeftInv (Substitution' Term, Substitution' Term)
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a b. (a -> b) -> a -> b
$ NoLeftInv
-> Either NoLeftInv (Substitution' Term, Substitution' Term)
forall a b. a -> Either a b
Left NoLeftInv
UnsupportedCxt) (TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
 -> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term)))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a b. (a -> b) -> a -> b
$ do
    equivs <- DigestedUnifyLog
-> ((DigestedUnifyLogEntry, UnifyState)
    -> TCMT IO (Either NoLeftInv (Retract, Term)))
-> TCMT IO [Either NoLeftInv (Retract, Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM DigestedUnifyLog
log (((DigestedUnifyLogEntry, UnifyState)
  -> TCMT IO (Either NoLeftInv (Retract, Term)))
 -> TCMT IO [Either NoLeftInv (Retract, Term)])
-> ((DigestedUnifyLogEntry, UnifyState)
    -> TCMT IO (Either NoLeftInv (Retract, Term)))
-> TCMT IO [Either NoLeftInv (Retract, Term)]
forall a b. (a -> b) -> a -> b
$ (DigestedUnifyLogEntry
 -> UnifyState -> TCMT IO (Either NoLeftInv (Retract, Term)))
-> (DigestedUnifyLogEntry, UnifyState)
-> TCMT IO (Either NoLeftInv (Retract, Term))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry DigestedUnifyLogEntry
-> UnifyState -> TCMT IO (Either NoLeftInv (Retract, Term))
buildEquiv
    case sequence equivs of
      Left NoLeftInv
no -> do
        [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv.badstep" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"No Left Inverse:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM (NoLeftInv -> UnifyStep
badStep NoLeftInv
no)
        Either NoLeftInv (Substitution' Term, Substitution' Term)
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv
-> Either NoLeftInv (Substitution' Term, Substitution' Term)
forall a b. a -> Either a b
Left NoLeftInv
no)
      Right [(Retract, Term)]
xs -> ExceptT NoLeftInv (TCMT IO) Retract
-> TCM (Either NoLeftInv Retract)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ([(Retract, Term)] -> ExceptT NoLeftInv (TCMT IO) Retract
compose [(Retract, Term)]
xs) TCM (Either NoLeftInv Retract)
-> (Either NoLeftInv Retract
    -> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term)))
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
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
        Left NoLeftInv
no -> Either NoLeftInv (Substitution' Term, Substitution' Term)
-> TCM (Either NoLeftInv (Substitution' Term, Substitution' Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv
-> Either NoLeftInv (Substitution' Term, Substitution' Term)
forall a b. a -> Either a b
Left NoLeftInv
no)
        Right (Tele (Dom Type)
_, Substitution' Term
_, Substitution' Term
tau0, Substitution' Term
leftInv0) -> do
        -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
        -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,1,refls][τ] = idS : Γ,φ,us =_Δ vs
        let tau :: Substitution' Term
tau = Substitution' Term
tau0 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1
        unview <- TCMT IO (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
        let replaceAt Int
n a
x [a]
xs = [a]
xs0 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++! (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs1)
                    where ([a]
xs0,a
_:[a]
xs1) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
n [a]
xs
        let max Term
r Term
s = 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
r) (Term -> Arg Term
forall e. e -> Arg e
argN Term
s)
            neg Term
r = IntervalView -> Term
unview (IntervalView -> Term) -> IntervalView -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> IntervalView
INeg (Term -> Arg Term
forall e. e -> Arg e
argN Term
r)
        let phieq = Term -> Term
neg (Int -> Term
var Int
0) Term -> Term -> Term
`max` Int -> Term
var (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Tele (Dom Type)
eqTel UnifyState
s0) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                          -- I + us =_Δ vs -- inplaceS
        let leftInv = Impossible -> [Term] -> Substitution' Term
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> [Term] -> [Term]
forall {a}. Int -> a -> [a] -> [a]
replaceAt (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Tele (Dom Type)
varTel UnifyState
s0)) Term
phieq ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' (Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
leftInv0) ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Tele (Dom Type)
varTel UnifyState
s0) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Tele (Dom Type)
eqTel UnifyState
s0))
        let working_tel = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract (UnifyState -> Tele (Dom Type)
varTel UnifyState
s0) (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs [Char]
"phi0" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ (UnifyState -> Tele (Dom Type)
eqTel UnifyState
s0))
        reportSDoc "tc.lhs.unify.inv" 20 $ "=== before mod"
        do
            reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "tau0    :" <+> prettyTCM tau0
            reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $ addContext ("r" :: String, __DUMMY_DOM__) $
              "leftInv0:  " <+> prettyTCM leftInv0

        reportSDoc "tc.lhs.unify.inv" 20 $ "=== after mod"
        do
            reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $ "tau    :" <+> prettyTCM tau
            reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $ addContext ("r" :: String, __DUMMY_DOM__) $
              "leftInv:   " <+> prettyTCM leftInv

        return $ Right (tau,leftInv)

type Retract = (Telescope, Substitution, Substitution, Substitution)
     -- Γ (the problem, including equalities),
     -- Δ ⊢ ρ : Γ
     -- Γ ⊢ τ : Δ
     -- Γ, i : I ⊢ leftInv : Γ, such that (λi. leftInv) : ρ[τ] = id_Γ

--- Γ ⊢ us : Δ   Γ ⊢ termsS e us : Δ
termsS ::  DeBruijn a => Impossible -> [a] -> Substitution' a
termsS :: forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
e [a]
xs = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
e

composeRetract :: Retract -> Term -> Retract -> TCM (Either (Closure (Abs Type)) Retract)
composeRetract :: Retract
-> Term -> Retract -> TCM (Either (Closure (Abs Type)) Retract)
composeRetract (Tele (Dom Type)
prob0,Substitution' Term
rho0,Substitution' Term
tau0,Substitution' Term
leftInv0) Term
phi0 (Tele (Dom Type)
prob1,Substitution' Term
rho1,Substitution' Term
tau1,Substitution' Term
leftInv1) = do
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"=== composing"
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Γ0   :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
prob0
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tau0  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
tau0
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Γ1   :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
prob1
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tau1  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
tau1


  {-
  Γ0 = prob0
  S0 ⊢ ρ0 : Γ0
  Γ0 ⊢ τ0 : S0
  Γ0 ⊢ leftInv0 : ρ0[τ0] = idΓ0
  Γ0 ⊢ φ0
  Γ0,φ0 ⊢ leftInv0 = refl

  Γ1 = prob1
  S1 ⊢ ρ1 : Γ1
  Γ1 ⊢ τ1 : S1
  Γ1 ⊢ leftInv1 : ρ1[τ1] = idΓ1
  Γ1 ⊢ φ1 = φ0[τ0] (**)
  Γ1,φ1 ⊢ leftInv1 = refl
  S0 = Γ1

  (**) implies?
  Γ0,φ0 ⊢ leftInv1[τ0] = refl  (*)


  S1 ⊢ ρ := ρ0[ρ1] : Γ0
  Γ0 ⊢ τ := τ1[τ0] : S1
  -}

  let prob :: Tele (Dom Type)
prob = Tele (Dom Type)
prob0
  let rho :: Substitution' Term
rho = Substitution' Term
rho1 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
rho0
  let tau :: Substitution' Term
tau = Substitution' Term
tau0 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
tau1

  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tau  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
tau

  {-
  Γ0 ⊢ leftInv : ρ[τ] = idΓ0
  Γ0 ⊢ leftInv : ρ0[ρ1[τ1]][τ0] = idΓ0
  Γ0 ⊢ step0 := ρ0[leftInv1[τ0]] : ρ0[ρ1[τ1]][τ0] = ρ0[τ0]

  Γ0,φ0 ⊢ step0 = refl     by (*)


  Γ0 ⊢ leftInv := step0 · leftInv0 : ρ0[ρ1[τ1]][τ0] = idΓ0

  Γ0 ⊢ leftInv := tr (\ i → ρ0[ρ1[τ1]][τ0] = leftInv0[i]) φ0 step0
  Γ0,φ0 ⊢ leftInv = refl  -- because it will become step0, which is refl when φ0

  Γ0, i : I ⊢ hcomp {Γ0} (\ j → \ { (i = 0) -> ρ0[ρ1[τ1]][τ0]
                                  ; (i = 1) -> leftInv0[j]
                                  ; (φ0 = 1) -> γ0
                                  })
                         (step0[i])




  -}
  let step0 :: Substitution' Term
step0 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' Term
tau0 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
leftInv1 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
rho0

  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ([Char], Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"leftInv0  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
leftInv0
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"rho0  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
rho0
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tau0  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
tau0
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"rhos0[tau0]  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM (Substitution' Term
tau0 Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
rho0)

  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ([Char], Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"leftInv1  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
leftInv1
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ([Char], Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"step0  :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
step0

  interval <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  max <- primIMax
  neg <- primINeg
  result <- sequenceA <$!> do
    addContext prob0 $ runNamesT (teleNames prob0) $ do
             phi <- open phi0
             g0 <- open $ raise (size prob0) prob0
             step0 <- open $ Abs "i" $ step0 `applySubst` teleArgs prob0
             leftInv0 <- open $ Abs "i" $ map' unArg $ leftInv0 `applySubst` teleArgs prob0
             bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> ([Char], Dom Type)
-> NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term])
-> NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term])
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"i" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
interval) (NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term])
 -> NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term]))
-> NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term])
-> NamesT (TCMT IO) (Either (Closure (Abs Type)) [Term])
forall a b. (a -> b) -> a -> b
$ do
              tel <- [Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
    -> NamesT (TCMT IO) (Tele (Dom Type)))
-> NamesT (TCMT IO) (Abs (Tele (Dom Type)))
forall (m :: * -> *) a.
Monad m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"_" (((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
  -> NamesT (TCMT IO) (Tele (Dom Type)))
 -> NamesT (TCMT IO) (Abs (Tele (Dom Type))))
-> ((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
    -> NamesT (TCMT IO) (Tele (Dom Type)))
-> NamesT (TCMT IO) (Abs (Tele (Dom Type)))
forall a b. (a -> b) -> a -> b
$ \ (NamesT (TCMT IO) Term
_ :: NamesT tcm Term) -> NamesT (TCMT IO) (Tele (Dom Type))
g0
              step0i <- lazyAbsApp <$!> step0 <*!> i
              face <- pure max <@> (pure neg <@> i) <@> phi
              leftInv0 <- leftInv0
              i <- i
              -- this composition could be optimized further whenever step0i is actually constant in i.
              lift $ runExceptT (map' unArg <$> transpSysTel' True tel [(i, leftInv0)] face step0i)
  case result of
    Left  Closure (Abs Type)
cl      -> Either (Closure (Abs Type)) Retract
-> TCM (Either (Closure (Abs Type)) Retract)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Closure (Abs Type) -> Either (Closure (Abs Type)) Retract
forall a b. a -> Either a b
Left Closure (Abs Type)
cl)
    Right Abs [Term]
leftInv -> do
      let sigma :: Substitution' Term
sigma = Impossible -> [Term] -> Substitution' Term
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Abs [Term] -> [Term]
forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv
      [Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.lhs.unify.inv" Int
20 do
        Tele (Dom Type) -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
prob0 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ([Char], Dom Type) -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"leftInv    :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM (Abs [Term] -> [Term]
forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv)
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"leftInv    :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Abs [Term] -> [Term]
forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv)
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"leftInvSub :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution' Term
sigma
      Either (Closure (Abs Type)) Retract
-> TCM (Either (Closure (Abs Type)) Retract)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Closure (Abs Type)) Retract
 -> TCM (Either (Closure (Abs Type)) Retract))
-> Either (Closure (Abs Type)) Retract
-> TCM (Either (Closure (Abs Type)) Retract)
forall a b. (a -> b) -> a -> b
$ Retract -> Either (Closure (Abs Type)) Retract
forall a b. b -> Either a b
Right (Tele (Dom Type)
prob, Substitution' Term
rho, Substitution' Term
tau, Substitution' Term
sigma)

-- | Build the left inverse corresponding to a single unification step.
buildEquiv :: DigestedUnifyLogEntry -> UnifyState -> TCM (Either NoLeftInv (Retract,Term))
buildEquiv :: DigestedUnifyLogEntry
-> UnifyState -> TCMT IO (Either NoLeftInv (Retract, Term))
buildEquiv (DUnificationStep UnifyState
st step :: DigestedUnifyStep
step@(DSolution Int
k Dom Type
ty FlexibleVar Int
fx Term
tm Either () ()
side) UnifyOutput
output) UnifyState
next = ExceptT NoLeftInv (TCMT IO) (Retract, Term)
-> TCMT IO (Either NoLeftInv (Retract, Term))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT NoLeftInv (TCMT IO) (Retract, Term)
 -> TCMT IO (Either NoLeftInv (Retract, Term)))
-> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
-> TCMT IO (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ do
        let
          cantTransport' :: ExceptT (Closure Type) TCM b -> ExceptT NoLeftInv TCM b
          cantTransport' :: forall b.
ExceptT (Closure Type) (TCMT IO) b -> ExceptT NoLeftInv (TCMT IO) b
cantTransport' ExceptT (Closure Type) (TCMT IO) b
m = (Closure Type -> NoLeftInv)
-> ExceptT (Closure Type) (TCMT IO) b
-> ExceptT NoLeftInv (TCMT IO) b
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT Closure Type -> NoLeftInv
CantTransport' ExceptT (Closure Type) (TCMT IO) b
m
          cantTransport :: ExceptT (Closure (Abs Type)) TCM b -> ExceptT NoLeftInv TCM b
          cantTransport :: forall b.
ExceptT (Closure (Abs Type)) (TCMT IO) b
-> ExceptT NoLeftInv (TCMT IO) b
cantTransport ExceptT (Closure (Abs Type)) (TCMT IO) b
m = (Closure (Abs Type) -> NoLeftInv)
-> ExceptT (Closure (Abs Type)) (TCMT IO) b
-> ExceptT NoLeftInv (TCMT IO) b
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT Closure (Abs Type) -> NoLeftInv
CantTransport ExceptT (Closure (Abs Type)) (TCMT IO) b
m

        [Char] -> Int -> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"step unifyState:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
st
        [Char] -> Int -> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"step step:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (UnifyState -> Tele (Dom Type)
varTel UnifyState
st) (DigestedUnifyStep -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DigestedUnifyStep -> m Doc
prettyTCM DigestedUnifyStep
step)
        unview <- ExceptT NoLeftInv (TCMT IO) (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
        cxt <- getContextTelescope
        reportSDoc "tc.lhs.unify.inv" 20 $ "context:" <+> prettyTCM cxt
        let
          m = UnifyState -> Int
varCount UnifyState
st
          gamma = UnifyState -> Tele (Dom Type)
varTel UnifyState
st
          eqs = UnifyState -> Tele (Dom Type)
eqTel UnifyState
st
          -- k counts in eqs from the left
          u = UnifyState -> [Arg Term]
eqLHS UnifyState
st [Arg Term] -> Int -> Arg Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          v = UnifyState -> [Arg Term]
eqRHS UnifyState
st [Arg Term] -> Int -> Arg Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          -- Γ ⊢ perm : Γ' is a reordering used by instantiateTelescope to ensure the
          -- resulting context is well-formed. Works on de Bruijn levels.
          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
$ UnifyOutput -> Maybe Permutation
unifySolutionPerm UnifyOutput
output
          -- The new de Bruijn index of fx in Γ'. The target context for τ is obtained by dropping
          -- x from Γ' (and the kth equation from the equation telescope) and instantiating
          -- it with u (resp. refl).
          x = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Permutation -> Int -> Maybe Int
lookupRP (Permutation -> Permutation
reverseP Permutation
perm) (FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fx)
          neqs = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
eqs
          phis = Int
1
        interval <- lift $ primIntervalType
         -- Γ, φ : I
        let gamma_phis = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gamma (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ListTel -> Tele (Dom Type)
telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$
              (Int -> Dom ([Char], Type)) -> [Int] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map' (([Char], Type) -> Dom ([Char], Type)
forall a. a -> Dom a
defaultDom (([Char], Type) -> Dom ([Char], Type))
-> (Int -> ([Char], Type)) -> Int -> Dom ([Char], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) ([Char] -> ([Char], Type))
-> (Int -> [Char]) -> Int -> ([Char], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"phi" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show) [Int
0 .. Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        -- working_tel = Γ, φ : I, eqs : lhs ≡ rhs
        working_tel <- abstract gamma_phis <$!>
          cantTransport' (pathTelescope' (raise phis $ eqTel st) (raise phis $ eqLHS st) (raise phis $ eqRHS st))
        -- working_tel' = Γ'           , φ : I, eqs : lhs ≡ rhs
        --              = Γ₁, x : A, Γ₂, φ : I, eqs : lhs ≡ rhs
        let permw = Int -> Permutation -> Permutation
liftP (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma) Permutation
perm
        working_tel' <- pure $ permuteTel permw working_tel
        reportSDoc "tc.lhs.unify.inv" 20 $ vcat
          [ "working tel:" <+> prettyTCM (working_tel :: Telescope)
          , addContext working_tel $ "working tel args:" <+> prettyTCM (teleArgs working_tel :: [Arg Term])
          , "perm:" <+> prettyTCM perm
          ]
        (tau,leftInv,phi) <- addContext working_tel $ runNamesT [] $ do
          let
            raiseFrom :: Subst a => Telescope -> a -> a
            raiseFrom Tele (Dom Type)
tel a
x = Int -> a -> a
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) a
x
            bindSplit (Tele (Dom Type)
tel1,a
tel2) = (Tele (Dom Type)
tel1,Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (Tele (Dom Type) -> Names
teleNames Tele (Dom Type)
tel1) a
tel2)
          u <- open . raiseFrom gamma . unArg $ u
          v <- open . raiseFrom gamma . unArg $ v
          -- φ
          let phi = Tele (Dom Type) -> Term -> Term
forall a. Subst a => Tele (Dom Type) -> a -> a
raiseFrom Tele (Dom Type)
gamma_phis (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
          -- working_tel ⊢ γ₁,x,γ₂,φ,eqs : working_tel'
          let all_args = Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute Permutation
permw ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
working_tel

          -- . ⊢ Γ₁  ,  γ₁. x : A, Γ₂, φ : I, eqs : lhs ≡ rhs
          let (gamma1, xxi) = bindSplit $ splitTelescopeAt (size gamma - x - 1) working_tel'
              (gamma1_args,xxi_args) = splitAt' (size gamma1) all_args
              (_x_arg:xi_args) = xxi_args
              (x_arg:xi0,k_arg:xi1) = splitAt' (size gamma - size gamma1 + phis + k) xxi_args
              -- working_tel ⊢ x : A, Γ₂, φ : I, eqs : lhs ≡ rhs
              xxi_here = AbsN (Tele (Dom Type))
-> [SubstArg (Tele (Dom Type))] -> Tele (Dom Type)
forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN (Tele (Dom Type))
xxi ([SubstArg (Tele (Dom Type))] -> Tele (Dom Type))
-> [SubstArg (Tele (Dom Type))] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ (Arg Term -> SubstArg (Tele (Dom Type)))
-> [Arg Term] -> [SubstArg (Tele (Dom Type))]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
Arg Term -> SubstArg (Tele (Dom Type))
forall e. Arg e -> e
unArg [Arg Term]
gamma1_args
              --                                                  x:A, Γ₂               φ
              (xpre,krest) = bindSplit $ splitTelescopeAt ((size gamma - size gamma1) + phis + k) xxi_here
          k_arg <- open $ unArg k_arg
          xpre <- open xpre
          krest <- open krest
          -- Δ₀ = Γ₁, Γ₂
          -- Δ  = x eq. Δ₀, φ : I, eqs-k : lhs-k ≡ rhs-k
          delta <- bindN ["x","eq"] $ \ [NamesT (ExceptT NoLeftInv (TCMT IO)) Term
x,NamesT (ExceptT NoLeftInv (TCMT IO)) Term
eq] -> do
                     let pre :: NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
pre = Tele (Dom Type) -> Term -> Tele (Dom Type)
forall t. Apply t => t -> Term -> t
apply1 (Tele (Dom Type) -> Term -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
xpre NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
x
                     NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
-> (Vars (ExceptT NoLeftInv (TCMT IO))
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type)))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a.
(Monad m, Abstract a) =>
NamesT m (Tele (Dom Type)) -> (Vars m -> NamesT m a) -> NamesT m a
abstractN NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
pre ((Vars (ExceptT NoLeftInv (TCMT IO))
  -> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type)))
 -> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type)))
-> (Vars (ExceptT NoLeftInv (TCMT IO))
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type)))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ \ Vars (ExceptT NoLeftInv (TCMT IO))
args ->
                       Tele (Dom Type) -> Term -> Tele (Dom Type)
forall t. Apply t => t -> Term -> t
apply1 (Tele (Dom Type) -> Term -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (AbsN (Tele (Dom Type)))
-> [NamesT
      (ExceptT NoLeftInv (TCMT IO)) (SubstArg (Tele (Dom Type)))]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT (ExceptT NoLeftInv (TCMT IO)) (AbsN (Tele (Dom Type)))
krest (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
xNamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
forall a. a -> [a] -> [a]
:[NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
Vars (ExceptT NoLeftInv (TCMT IO))
args) NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
eq
          -- working_tel ⊢ delta0_args : Δ₀
          let delta0_args = [Arg Term]
xi0 [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++! [Arg Term]
xi1
          let appSide = case Either () ()
side of
                          Left{} -> Term -> Term
forall a. a -> a
id
                          Right{} -> IntervalView -> Term
unview (IntervalView -> Term) -> (Term -> IntervalView) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> IntervalView
INeg (Arg Term -> IntervalView)
-> (Term -> Arg Term) -> Term -> IntervalView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall e. e -> Arg e
argN
          let
                  -- csingl :: NamesT tcm Term -> NamesT tcm [Arg Term]
                  csingl NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i = (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
 -> NamesT (ExceptT NoLeftInv (TCMT IO)) (Arg Term))
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [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 ((Term -> Arg Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Arg Term)
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) a
-> NamesT (ExceptT NoLeftInv (TCMT IO)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Arg Term
forall e. e -> Arg e
defaultArg) ([NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
 -> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term])
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall a b. (a -> b) -> a -> b
$ NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
csingl' NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i
                  -- csingl' :: NamesT tcm Term -> [NamesT tcm Term]
                  csingl' NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i = [ NamesT (ExceptT NoLeftInv (TCMT IO)) Term
k_arg NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term,
    NamesT (ExceptT NoLeftInv (TCMT IO)) Term,
    NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
u, NamesT (ExceptT NoLeftInv (TCMT IO)) Term
v, Term -> Term
appSide (Term -> Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i)
                              , [Char]
-> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *).
Monad m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" ((NamesT (ExceptT NoLeftInv (TCMT IO)) Term
  -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
 -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT NoLeftInv (TCMT IO)) Term
j ->
                                  let r :: Term -> Term -> Term
r Term
i Term
j = case Either () ()
side of
                                            Left{} -> IntervalView -> Term
unview (Arg Term -> Arg Term -> IntervalView
IMax (Term -> Arg Term
forall e. e -> Arg e
argN Term
j) (Term -> Arg Term
forall e. e -> Arg e
argN Term
i))
                                            Right{} -> IntervalView -> Term
unview (Arg Term -> Arg Term -> IntervalView
IMin (Term -> Arg Term
forall e. e -> Arg e
argN Term
j) (Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term)
-> (IntervalView -> Term) -> IntervalView -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntervalView -> Term
unview (IntervalView -> Arg Term) -> IntervalView -> Arg Term
forall a b. (a -> b) -> a -> b
$ 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
i))
                                  in NamesT (ExceptT NoLeftInv (TCMT IO)) Term
k_arg NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term,
    NamesT (ExceptT NoLeftInv (TCMT IO)) Term,
    NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
u, NamesT (ExceptT NoLeftInv (TCMT IO)) Term
v, Term -> Term -> Term
r (Term -> Term -> Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Term)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
j)
                              ]
          let replaceAt Int
n a
x [a]
xs = [a]
xs0 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++! (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs1)
                where ([a]
xs0,a
_:[a]
xs1) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
n [a]
xs
              dropAt Int
n [a]
xs = [a]
xs0 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++! [a]
xs1
                where ([a]
xs0,a
_:[a]
xs1) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
n [a]
xs
          delta <- open delta
          -- d = i. Δ (k i) (λ j → k (i ∧ j))
          d <- bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> NamesT (ExceptT NoLeftInv (TCMT IO)) (AbsN (Tele (Dom Type)))
-> [NamesT
      (ExceptT NoLeftInv (TCMT IO)) (SubstArg (Tele (Dom Type)))]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT (ExceptT NoLeftInv (TCMT IO)) (AbsN (Tele (Dom Type)))
delta (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
csingl' NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i)

          -- Andrea 06/06/2018
          -- We do not actually add a transp/fill if the family is
          -- constant (TODO: postpone for metas) This is so variables
          -- whose types do not depend on "x" are left alone, in
          -- particular those the solution "t" depends on.
          --
          -- We might want to instead use the info discovered by instantiateTelescope
          -- when checking if "t" depends on "x" to decide what
          -- to transp and what not to.
          let flag = Bool
True
          tau <- (gamma1_args ++!) <$!> lift (cantTransport (transpTel' flag d phi delta0_args))
          reportSDoc "tc.lhs.unify.inv" 20 $ "tau    :" <+> prettyTCM (map (setHiding NotHidden) tau)
          leftInv <- do
            gamma1_args <- open gamma1_args
            phi <- open phi
            -- xxi_here <- open xxi_here
            -- (xi_here_f :: Abs Telescope) <- bind "i" $ \ i -> apply <$> xxi_here <*> (take' 1 `fmap` csingl i)
            -- xi_here_f <- open xi_here_f
            -- xi_args <- open xi_args
            -- xif <- bind "i" $ \ i -> do
            --                      m <- (runExceptT <$> (trFillTel' flag <$> xi_here_f <*> phi <*> xi_args <*> i))
            --                      either __IMPOSSIBLE__ id <$> lift m
            -- xif <- open xif

            xi0 <- open xi0
            xi1 <- open xi1
            delta0 <- bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
forall t. Apply t => t -> [Arg Term] -> t
apply (Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
-> NamesT
     (ExceptT NoLeftInv (TCMT IO)) ([Arg Term] -> Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
xpre NamesT
  (ExceptT NoLeftInv (TCMT IO)) ([Arg Term] -> Tele (Dom Type))
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Tele (Dom Type))
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> (Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take' Int
1 ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
csingl NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i)
            delta0 <- open delta0
            xi0f <- bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> do
                                 m <- Bool
-> Abs (Tele (Dom Type))
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs (Tele (Dom Type))
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag (Abs (Tele (Dom Type))
 -> Term
 -> [Arg Term]
 -> Term
 -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs (Tele (Dom Type)))
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (Term
      -> [Arg Term]
      -> Term
      -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs (Tele (Dom Type)))
delta0 NamesT
  (ExceptT NoLeftInv (TCMT IO))
  (Term
   -> [Arg Term]
   -> Term
   -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     ([Arg Term]
      -> Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
phi NamesT
  (ExceptT NoLeftInv (TCMT IO))
  ([Arg Term]
   -> Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
xi0 NamesT
  (ExceptT NoLeftInv (TCMT IO))
  (Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i
                                 lift (cantTransport m)
            xi0f <- open xi0f

            delta1 <- bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> do

                   args <- (Arg Term
 -> NamesT
      (ExceptT NoLeftInv (TCMT IO))
      (NamesT (ExceptT NoLeftInv (TCMT IO)) Term))
-> [Arg Term]
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     [NamesT (ExceptT NoLeftInv (TCMT IO)) 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 (Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term
 -> NamesT
      (ExceptT NoLeftInv (TCMT IO))
      (NamesT (ExceptT NoLeftInv (TCMT IO)) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) ([Arg Term]
 -> NamesT
      (ExceptT NoLeftInv (TCMT IO))
      [NamesT (ExceptT NoLeftInv (TCMT IO)) Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     [NamesT (ExceptT NoLeftInv (TCMT IO)) Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Abs [Arg Term] -> Term -> [Arg Term]
Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
xi0f NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i)
                   apply <$> applyN krest (take' 1 (csingl' i) ++! args) <*!> (drop 1 <$!> csingl i)
            delta1 <- open delta1
            xi1f <- bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> do
                                 m <- Bool
-> Abs (Tele (Dom Type))
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs (Tele (Dom Type))
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag (Abs (Tele (Dom Type))
 -> Term
 -> [Arg Term]
 -> Term
 -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs (Tele (Dom Type)))
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (Term
      -> [Arg Term]
      -> Term
      -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs (Tele (Dom Type)))
delta1 NamesT
  (ExceptT NoLeftInv (TCMT IO))
  (Term
   -> [Arg Term]
   -> Term
   -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     ([Arg Term]
      -> Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
phi NamesT
  (ExceptT NoLeftInv (TCMT IO))
  ([Arg Term]
   -> Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
xi1 NamesT
  (ExceptT NoLeftInv (TCMT IO))
  (Term -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT
     (ExceptT NoLeftInv (TCMT IO))
     (ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i
                                 lift (cantTransport m)
            xi1f <- open xi1f
            fmap absBody $ bind "i" $ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i' -> do
              let +++ :: m [a] -> m [a] -> m [a]
(+++) m [a]
m = ([a] -> [a] -> [a]) -> m [a] -> m [a] -> m [a]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++!) m [a]
m
                  i :: NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i = ExceptT NoLeftInv (TCMT IO) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl (TCMT IO Term -> ExceptT NoLeftInv (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> ExceptT NoLeftInv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg) NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i'
              ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) a
-> NamesT (ExceptT NoLeftInv (TCMT IO)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
invertP Int
forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
permw)) (NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
 -> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall a b. (a -> b) -> a -> b
$
                NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
gamma1_args NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
+++ ((Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take' Int
1 ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
csingl NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i) NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
+++ ((Abs [Arg Term] -> Term -> [Arg Term]
Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
xi0f NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i) NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
+++ ((Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop Int
1 ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
csingl NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i) NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
+++ (Abs [Arg Term] -> Term -> [Arg Term]
Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs [Arg Term])
xi1f NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i))))
          return (tau,leftInv,phi)
        iz <- lift $ primIZero
        io <- lift $ primIOne
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "tau    :" <+> prettyTCM (map (setHiding NotHidden) tau)
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "tauS   :" <+> prettyTCM (termsS __IMPOSSIBLE__ $ map unArg tau)
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $ addContext ("r" :: String, defaultDom interval) $
           "leftInv:   " <+> prettyTCM (map (setHiding NotHidden) leftInv)
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "leftInv[0]:" <+> (prettyTCM =<< reduce (subst 0 iz $ map (setHiding NotHidden) leftInv))
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "leftInv[1]:" <+> (prettyTCM =<< reduce  (subst 0 io $ map (setHiding NotHidden) leftInv))
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext working_tel $  "[rho]tau :" <+>
          prettyTCM (applySubst (termsS __IMPOSSIBLE__ $ map unArg tau) $ fromPatternSubstitution
                                                                      $ raise (size (eqTel st) - 1 + phis)
                                                                      $ unifySubst output)
        reportSDoc "tc.lhs.unify.inv" 20 $ "."
        let rho0 = PatternSubstitution -> Substitution' Term
fromPatternSubstitution (PatternSubstitution -> Substitution' Term)
-> PatternSubstitution -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output
        reportSDoc "tc.lhs.unify.inv" 20 $ addContext (varTel next) $ addContext (eqTel next) $
          "prf :" <+> prettyTCM (fromPatternSubstitution $ unifyProof output)
        let c0 = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS (PatternSubstitution -> Substitution' Term
fromPatternSubstitution (PatternSubstitution -> Substitution' Term)
-> PatternSubstitution -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
output) (Int
neqs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        let c = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (Tele (Dom Type) -> Int) -> Tele (Dom Type) -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Tele (Dom Type)
eqTel UnifyState
next) (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1) Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
c0
        reportSDoc "tc.lhs.unify.inv" 20 $
          addContext (varTel next) $ addContext ("φ" :: String, __DUMMY_DOM__) $ addContext (raise 1 $ eqTel next) $
            "c :" <+> prettyTCM c
        let rho = Int -> Term -> Substitution' Term
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS (Int
neqs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
c  Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
neqs) Substitution' Term
rho0
        reportSDoc "tc.lhs.unify.inv" 20 $ text "old_sizes: " <+> pretty (size $ varTel st, size $ eqTel st)
        reportSDoc "tc.lhs.unify.inv" 20 $ text "new_sizes: " <+> pretty (size $ varTel next, size $ eqTel next)
        reportSDoc "tc.lhs.unify.inv" 20 $
          addContext (varTel next) $ addContext ("φ" :: String, __DUMMY_DOM__) $ addContext (raise 1 $ eqTel next) $
            "rho   :" <+> prettyTCM rho
        return ((working_tel
                , rho
                , termsS __IMPOSSIBLE__ $ map' unArg tau
                , termsS __IMPOSSIBLE__ $ map' unArg leftInv)
                , phi)
buildEquiv (DUnificationStep UnifyState
st step :: DigestedUnifyStep
step@(DEtaExpandVar FlexibleVar Int
fv QName
_d [Arg Term]
_args) UnifyOutput
output) UnifyState
next = ExceptT NoLeftInv (TCMT IO) (Retract, Term)
-> TCMT IO (Either NoLeftInv (Retract, Term))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT NoLeftInv (TCMT IO) (Retract, Term)
 -> TCMT IO (Either NoLeftInv (Retract, Term)))
-> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
-> TCMT IO (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 TCM Doc
"buildEquiv EtaExpandVar"
        let
          gamma :: Tele (Dom Type)
gamma = UnifyState -> Tele (Dom Type)
varTel UnifyState
st
          eqs :: Tele (Dom Type)
eqs = UnifyState -> Tele (Dom Type)
eqTel UnifyState
st
          x :: Int
x = FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fv
          neqs :: Int
neqs = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
eqs
          phis :: Int
phis = Int
1
        interval <- TCMT IO Type -> ExceptT NoLeftInv (TCMT IO) Type
forall (m :: * -> *) a. Monad m => m a -> ExceptT NoLeftInv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
         -- Γ, φs : I^phis
        let gamma_phis = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gamma (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ListTel -> Tele (Dom Type)
telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$
              (Int -> Dom ([Char], Type)) -> [Int] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map' (([Char], Type) -> Dom ([Char], Type)
forall a. a -> Dom a
defaultDom (([Char], Type) -> Dom ([Char], Type))
-> (Int -> ([Char], Type)) -> Int -> Dom ([Char], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) ([Char] -> ([Char], Type))
-> (Int -> [Char]) -> Int -> ([Char], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"phi" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show) [Int
0 .. Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        working_tel <- abstract gamma_phis <$!> do
         withExceptT CantTransport' $
          pathTelescope' (raise phis $ eqTel st) (raise phis $ eqLHS st) (raise phis $ eqRHS st)
        let raiseFrom Tele (Dom Type)
tel Int
x = (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
x
        let phi = Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Int -> Int
raiseFrom Tele (Dom Type)
gamma_phis Int
0

        caseMaybeM (expandRecordVar (raiseFrom gamma x) working_tel) __IMPOSSIBLE__ $ \ (Tele (Dom Type)
_,Substitution' Term
tau,Substitution' Term
rho,Tele (Dom Type)
_) -> do
          [Char] -> Int -> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.lhs.unify.inv" Int
20 (TCM Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCM Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
working_tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tau    :" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' Term -> m Doc
prettyTCM Substitution' Term
tau
          (Retract, Term) -> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
forall a. a -> ExceptT NoLeftInv (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Retract, Term) -> ExceptT NoLeftInv (TCMT IO) (Retract, Term))
-> (Retract, Term) -> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
forall a b. (a -> b) -> a -> b
$ ((Tele (Dom Type)
working_tel,Substitution' Term
rho,Substitution' Term
tau,Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1),Term
phi)


{-# SPECIALIZE explainStep :: UnifyStep -> TCM Doc #-}
explainStep :: MonadPretty m => UnifyStep -> m Doc
explainStep :: forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
explainStep Injectivity{injectConstructor :: UnifyStep -> ConHead
injectConstructor = ConHead
ch} =
  m Doc
"injectivity of the data constructor" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (ConHead -> QName
conName ConHead
ch)
explainStep TypeConInjectivity{} = m Doc
"injectivity of type constructors"
explainStep Deletion{}           = m Doc
"the K rule"
explainStep Solution{}           = m Doc
"substitution in Setω"
-- Note: this is the actual reason that a Solution step can fail, rather
-- than the explanation for the actual step
explainStep Conflict{}          = m Doc
"the disjointness of data constructors"
explainStep LitConflict{}       = m Doc
"the disjointness of literal values"
explainStep Cycle{}             = m Doc
"the impossibility of cyclic values"
explainStep EtaExpandVar{}      = m Doc
"eta-expansion of variables"
explainStep EtaExpandEquation{} = m Doc
"eta-expansion of equations"
explainStep StripSizeSuc{}      = m Doc
"the injectivity of size successors"
explainStep SkipIrrelevantEquation{} = m Doc
"ignoring irrelevant equations"