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

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

module Mikan.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 Data.Text.Short (ShortText)

import Mikan.TypeChecking.Monad.Benchmark qualified as Bench

import Mikan.Syntax.Common
import Mikan.Syntax.Internal

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

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

import Mikan.Utils.List
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Permutation
import Mikan.Utils.Size
import Mikan.Utils.Suffix

import Mikan.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__
    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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is not yet supported"
  prettyTCM NoLeftInv
UnsupportedCxt     = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is incompatible with" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cubical Agda"]
  prettyTCM NoLeftInv
NoCubical          = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Cubical Agda is disabled"
  prettyTCM NoLeftInv
WithKEnabled       = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"The K rule is enabled"
  prettyTCM NoLeftInv
SplitOnStrict      = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"It splits on a type in SSet"
  prettyTCM NoLeftInv
SplitOnFlat        = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"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 -> String
(Int -> NoLeftInv -> ShowS)
-> (NoLeftInv -> String)
-> ([NoLeftInv] -> ShowS)
-> Show NoLeftInv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoLeftInv -> ShowS
showsPrec :: Int -> NoLeftInv -> ShowS
$cshow :: NoLeftInv -> String
show :: NoLeftInv -> String
$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, Substitution))
buildLeftInverse UnifyState
s0 UnifyLog
log = Account (BenchPhase (TCMT IO))
-> TCM (Either NoLeftInv (Substitution, Substitution))
-> TCM (Either NoLeftInv (Substitution, Substitution))
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, Substitution))
 -> TCM (Either NoLeftInv (Substitution, Substitution)))
-> TCM (Either NoLeftInv (Substitution, Substitution))
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a b. (a -> b) -> a -> b
$ case UnifyLog -> Either NoLeftInv DigestedUnifyLog
digestUnifyLog UnifyLog
log of
  Left NoLeftInv
no -> do
    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"No Left Inverse:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCMT IO 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, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
no)
  Right DigestedUnifyLog
log -> do

    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO 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, Substitution))
-> TCM (Either NoLeftInv (Substitution, Substitution))
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
cond (Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NoLeftInv (Substitution, Substitution)
 -> TCM (Either NoLeftInv (Substitution, Substitution)))
-> Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a b. (a -> b) -> a -> b
$ NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
UnsupportedCxt) (TCM (Either NoLeftInv (Substitution, Substitution))
 -> TCM (Either NoLeftInv (Substitution, Substitution)))
-> TCM (Either NoLeftInv (Substitution, Substitution))
-> TCM (Either NoLeftInv (Substitution, Substitution))
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
        String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"No Left Inverse:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCMT IO 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, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
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, Substitution)))
-> TCM (Either NoLeftInv (Substitution, Substitution))
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, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
no)
        Right (Telescope
_, Substitution
_, Substitution
tau0, Substitution
leftInv0) -> do
        -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
        -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,1,refls][τ] = idS : Γ,φ,us =_Δ vs
        unview <- TCMT IO (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
        let
          tau = Substitution
tau0 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1
          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)
          phieq = Term -> Term
neg (Int -> Term
var Int
0) Term -> Term -> Term
`max` Int -> Term
var (Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s0) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

          leftInv = Impossible -> [Term] -> Substitution
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__
            ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ Int -> Term -> [Term] -> [Term]
forall a. Int -> a -> [a] -> [a]
replaceAt' (Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
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 -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution
leftInv0)
            ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
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
+ Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s0))

          working_tel = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract (UnifyState -> Telescope
varTel UnifyState
s0) (Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ShortText -> Telescope -> Abs Telescope
forall a. ShortText -> a -> Abs a
Abs ShortText
"phi0" (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ (UnifyState -> Telescope
eqTel UnifyState
s0))

        reportSDoc "tc.lhs.unify.inv.compose" 30 $ addContext working_tel $ vcat
          [ "=== before mod"
          , "tau0    :" <+> prettyTCM tau0
          , addContext ("r" :: ShortText, __DUMMY_DOM__) $ "leftInv0:  " <+> prettyTCM leftInv0
          , "=== after mod"
          , "tau    :" <+> prettyTCM tau
          , addContext ("r" :: ShortText, __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 (Telescope
prob0,Substitution
rho0,Substitution
tau0,Substitution
leftInv0) Term
phi0 (Telescope
prob1,Substitution
rho1,Substitution
tau1,Substitution
leftInv1) = String
-> Int
-> String
-> TCM (Either (Closure (Abs Type)) Retract)
-> TCM (Either (Closure (Abs Type)) Retract)
forall a. String -> Int -> String -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.lhs.unify.inv" Int
20 String
"composing" do
  String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"=== composing"
    , TCMT IO Doc
"Γ0   :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
prob0
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau0  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
tau0
    , TCMT IO Doc
"Γ1   :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
prob1
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau1  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
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 rho :: Substitution
rho = Substitution
rho1 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
rho0
  let tau :: Substitution
tau = Substitution
tau0 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
tau1

  String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.compose" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
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
step0 = Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution
tau0 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
leftInv1 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
rho0

  String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.compose" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (ShortText, Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"r" :: ShortText, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv0  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
leftInv0
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rho0  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
rho0
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau0  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
tau0
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rhos0[tau0]  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM (Substitution
tau0 Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
rho0)
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (ShortText, Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"r" :: ShortText, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv1  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
leftInv1
    , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (ShortText, Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"r" :: ShortText, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"step0  :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
step0
    ]

  interval <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  result <- (<$!>) sequenceA $ 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 -> (ShortText, 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 =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"i" :: ShortText, Type -> Dom Type
forall a t. a -> Dom' t 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 <- ShortText
-> ((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
    -> NamesT (TCMT IO) Telescope)
-> NamesT (TCMT IO) (Abs Telescope)
forall (m :: * -> *) a.
Monad m =>
ShortText
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ShortText
"_" (((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
  -> NamesT (TCMT IO) Telescope)
 -> NamesT (TCMT IO) (Abs Telescope))
-> ((forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b)
    -> NamesT (TCMT IO) Telescope)
-> NamesT (TCMT IO) (Abs Telescope)
forall a b. (a -> b) -> a -> b
$ \ (NamesT (TCMT IO) Term
_ :: NamesT tcm Term) -> NamesT (TCMT IO) Telescope
g0
      step0i <- lazyAbsApp <$!> step0 <*!> i
      face <- imax (ineg 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
sigma = Impossible -> [Term] -> Substitution
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ Abs [Term] -> [Term]
forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv
      String -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"tc.lhs.unify.inv.compose" Int
30 do
        Telescope -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
prob0 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (ShortText, Dom Type) -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
"r" :: ShortText, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) do
          String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv    :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM (Abs [Term] -> [Term]
forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv)
          String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv    :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO 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)
          String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInvSub :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
sigma
      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 (Telescope
prob0, Substitution
rho, Substitution
tau, Substitution
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 st :: UnifyState
st@UState{varTel :: UnifyState -> Telescope
varTel = Telescope
gamma} 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
  String
-> Int
-> String
-> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
-> ExceptT NoLeftInv (TCMT IO) (Retract, Term)
forall a.
String
-> Int
-> String
-> ExceptT NoLeftInv (TCMT IO) a
-> ExceptT NoLeftInv (TCMT IO) a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.lhs.unify.inv" Int
20 String
"buildEquiv Solution" do
  String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.build" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"step unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
st
    , TCMT IO Doc
"step step:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (DigestedUnifyStep -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DigestedUnifyStep -> m Doc
prettyTCM DigestedUnifyStep
step)
    , TCMT IO Doc
"context:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Context -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Context -> m Doc
prettyTCM (Context -> TCMT IO Doc) -> TCMT IO Context -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext)
    ]
  unview <- ExceptT NoLeftInv (TCMT IO) (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'

  let
    cantTransport' :: ExceptT (Closure Type) TCM b -> ExceptT NoLeftInv TCM 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 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

    appSide = case Either () ()
side of
      Left{}  -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall a. a -> a
id
      Right{} -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg

    !nvars = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma
    !neqs  = Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
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)
    phis = Int
1

  interval <- lift primIntervalType
    -- Γ, φ : I
  let
    gamma_phis = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$
      (Integer -> Dom (ShortText, Type)) -> [Integer] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map' ((ShortText, Type) -> Dom (ShortText, Type)
forall a t. a -> Dom' t a
defaultDom ((ShortText, Type) -> Dom (ShortText, Type))
-> (Integer -> (ShortText, Type))
-> Integer
-> Dom (ShortText, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) (ShortText -> (ShortText, Type))
-> (Integer -> ShortText) -> Integer -> (ShortText, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Suffix -> ShortText
addSuffix ShortText
"phi" (Suffix -> ShortText)
-> (Integer -> Suffix) -> Integer -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Suffix
Index) [Integer
0 .. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
phis Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
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 (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nvars) Permutation
perm
    working_tel' = Permutation -> Telescope -> Telescope
permuteTel Permutation
permw Telescope
working_tel
    rho0 = PatternSubstitution -> Substitution
fromPatternSubstitution (PatternSubstitution -> Substitution)
-> PatternSubstitution -> Substitution
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output

  reportSDoc "tc.lhs.unify.inv.build" 30 $ 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 Telescope
tel a
x = Int -> a -> a
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) a
x
      bindSplit (Telescope
tel1,a
tel2) = (Telescope
tel1,Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (Telescope -> Names
teleNames Telescope
tel1) a
tel2)
    u <- open . raiseFrom gamma . unArg $ u
    v <- open . raiseFrom gamma . unArg $ v
    let
      -- φ
      phi = Telescope -> Term -> Term
forall a. Subst a => Telescope -> a -> a
raiseFrom Telescope
gamma_phis (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
      -- working_tel ⊢ γ₁,x,γ₂,φ,eqs : working_tel'
      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
$ Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
working_tel

      -- . ⊢ Γ₁  ,  γ₁. x : A, Γ₂, φ : I, eqs : lhs ≡ rhs
      (gamma1, xxi) = bindSplit $ splitTelescopeAt (nvars - x - 1) working_tel'
      !nvars1 = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma1

      (gamma1_args,xxi_args) = splitAt' nvars1 all_args
      (_x_arg:xi_args) = xxi_args
      (x_arg:xi0,k_arg:xi1) = splitAt' (nvars - nvars1 + phis + k) xxi_args

      -- working_tel ⊢ x : A, Γ₂, φ : I, eqs : lhs ≡ rhs
      xxi_here = AbsN Telescope -> [SubstArg Telescope] -> Telescope
forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN Telescope
xxi ([SubstArg Telescope] -> Telescope)
-> [SubstArg Telescope] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Arg Term -> SubstArg Telescope)
-> [Arg Term] -> [SubstArg Telescope]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
Arg Term -> SubstArg Telescope
forall e. Arg e -> e
unArg [Arg Term]
gamma1_args
      --                                                  x:A, Γ₂               φ
      (xpre,krest) = bindSplit $ splitTelescopeAt ((nvars - nvars1) + 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 <- open =<< 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)) Telescope
pre = Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
apply1 (Telescope -> Term -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Telescope)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
xpre NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
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)) Telescope
-> (Vars (ExceptT NoLeftInv (TCMT IO))
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
forall (m :: * -> *) a.
(Monad m, Abstract a) =>
NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
abstractN NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
pre \ Vars (ExceptT NoLeftInv (TCMT IO))
args ->
        Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
apply1 (Telescope -> Term -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Term -> Telescope)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) (AbsN Telescope)
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) (SubstArg Telescope)]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
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 Telescope)
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 -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
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

      -- contractibility of singletons for the solved variable.
      --
      -- note: the generated context for trX clauses assigns line types
      -- ((i : I) → ...) to the indices, instead of PathP (λ i → ...)
      -- types. this makes checkInternal complain about the IApply elim
      -- below.
      --
      -- however, without the IApply elim, we lose the information that
      -- the filler below is constant on its j endpoints. this makes
      -- checkInternal complain about the transp instead.
      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 (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, NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
appSide NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i)
        , ShortText
-> (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
    -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *).
Monad m =>
ShortText -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ShortText
"j" \ NamesT (ExceptT NoLeftInv (TCMT IO)) Term
j -> do
            let
              r :: NamesT (ExceptT NoLeftInv (TCMT IO)) Term
r = case Either () ()
side of
                Left{}  -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT (ExceptT NoLeftInv (TCMT IO)) Term
j NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i
                Right{} -> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT (ExceptT NoLeftInv (TCMT IO)) Term
j (NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg 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, NamesT (ExceptT NoLeftInv (TCMT IO)) Term
r)
        ]

    -- 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 Telescope)
-> [NamesT (ExceptT NoLeftInv (TCMT IO)) (SubstArg Telescope)]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
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 Telescope)
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 <- map' unArg <$!> do
      pure gamma1_args <++!> lift (cantTransport (transpTel' flag d phi delta0_args))
    reportSDoc "tc.lhs.unify.inv.build" 30 $ "tau    :" <+> prettyTCM tau

    leftInv <- do
      gamma1_args <- open gamma1_args
      phi <- open phi

      xi0 <- open xi0
      xi1 <- open xi1

      delta0 <- open =<< bind "i" \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i ->
        Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
apply (Telescope -> [Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
-> NamesT (ExceptT NoLeftInv (TCMT IO)) ([Arg Term] -> Telescope)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
xpre NamesT (ExceptT NoLeftInv (TCMT IO)) ([Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Telescope
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)

      xi0f <- open =<< bind "i" \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> do
        m <- Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag (Abs Telescope
 -> Term
 -> [Arg Term]
 -> Term
 -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs Telescope)
-> 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 Telescope)
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)

      delta1 <- open =<< 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)

      xi1f <- open =<< bind "i" \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i -> do
        m <- Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag (Abs Telescope
 -> Term
 -> [Arg Term]
 -> Term
 -> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) (Abs Telescope)
-> 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 Telescope)
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)

      bind' "i" \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i' -> do
        let i :: NamesT (ExceptT NoLeftInv (TCMT IO)) Term
i = NamesT (ExceptT NoLeftInv (TCMT IO)) Term
-> NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT (ExceptT NoLeftInv (TCMT IO)) Term
forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv (TCMT IO)) b
i'
        ([Arg Term] -> [Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [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 ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term])
-> ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)) [Term])
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [Arg Term]
-> NamesT (ExceptT NoLeftInv (TCMT IO)) [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

    reportSDoc "tc.lhs.unify.inv.build" 30 $ vcat
      [ "tau        =" <+> prettyTCM tau
      , "tauS       =" <+> prettyTCM (termsS __IMPOSSIBLE__ tau)
      , "leftInv    =" <+> do
          addContext ("r" :: ShortText, defaultDom interval) $ prettyTCM leftInv
      , "leftInv[0] =" <+> do
          iz <- primIZero
          prettyTCM =<< reduce (subst 0 iz leftInv)
      , "leftInv[1] =" <+> do
          io <- primIOne
          prettyTCM =<< reduce (subst 0 io leftInv)
      , "[rho]tau   =" <+> do
          prettyTCM $ applySubst (termsS __IMPOSSIBLE__ tau)
            $ raise (neqs - 1 + phis) rho0
      ]

    return (tau,leftInv,phi)

  let
    c0 = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ShortText -> Term -> Abs Term
forall a. ShortText -> a -> Abs a
Abs ShortText
"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 -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS (PatternSubstitution -> Substitution
fromPatternSubstitution (PatternSubstitution -> Substitution)
-> PatternSubstitution -> Substitution
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)
    c = Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
next) (Int -> Substitution
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
    rho = Int -> Term -> Substitution
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 -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
neqs) Substitution
rho0

  reportSDoc "tc.lhs.unify.inv.build" 30 $ addContext (varTel next) $ vcat
    [ "old_sizes =" <+> pretty (size $ varTel st, size $ eqTel st)
    , "new_sizes =" <+> pretty (size $ varTel next, size $ eqTel next)
    , "prf =" <+> do
        addContext (eqTel next) $ prettyTCM (fromPatternSubstitution $ unifyProof output)
    , "c   =" <+> do
        addContext ("φ" :: ShortText, defaultDom interval)
          $ addContext (raise 1 $ eqTel next)
          $ prettyTCM c
    , "rho = " <+> do
        addContext ("φ" :: ShortText, defaultDom interval)
          $ addContext (raise 1 $ eqTel next)
          $ prettyTCM rho
    ]

  let
    !tauS  = Impossible -> [Term] -> Substitution
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ [Term]
tau
    !linvS = Impossible -> [Term] -> Substitution
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ [Term]
leftInv
  pure ((working_tel, rho, tauS, linvS), phi)

buildEquiv (DUnificationStep st :: UnifyState
st@UState{varTel :: UnifyState -> Telescope
varTel = Telescope
gamma, [Arg Term]
FlexibleVars
Telescope
eqTel :: UnifyState -> Telescope
eqLHS :: UnifyState -> [Arg Term]
eqRHS :: UnifyState -> [Arg Term]
flexVars :: FlexibleVars
eqTel :: Telescope
eqLHS :: [Arg Term]
eqRHS :: [Arg Term]
flexVars :: UnifyState -> FlexibleVars
..} 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
  String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 TCMT IO Doc
"buildEquiv EtaExpandVar"
  String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.build" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"step unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
st
    , TCMT IO Doc
"step step:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (DigestedUnifyStep -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DigestedUnifyStep -> m Doc
prettyTCM DigestedUnifyStep
step)
    , TCMT IO Doc
"context:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Context -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Context -> m Doc
prettyTCM (Context -> TCMT IO Doc) -> TCMT IO Context -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext)
    ]

  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

  let
    x = FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fv
    neqs = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel
    phis = Int
1
    -- Γ, φs : I^phis

  let gamma_phis = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$
        (Integer -> Dom (ShortText, Type)) -> [Integer] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map' ((ShortText, Type) -> Dom (ShortText, Type)
forall a t. a -> Dom' t a
defaultDom ((ShortText, Type) -> Dom (ShortText, Type))
-> (Integer -> (ShortText, Type))
-> Integer
-> Dom (ShortText, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) (ShortText -> (ShortText, Type))
-> (Integer -> ShortText) -> Integer -> (ShortText, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Suffix -> ShortText
addSuffix ShortText
"phi" (Suffix -> ShortText)
-> (Integer -> Suffix) -> Integer -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Suffix
Index) [Integer
0 .. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
phis Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1]

  working_tel <- abstract gamma_phis <$!> withExceptT CantTransport' do
    pathTelescope' (raise phis eqTel) (raise phis eqLHS) (raise phis eqRHS)

  let raiseFrom Telescope
tel Int
x = (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
working_tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
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
$ Telescope -> Int -> Int
raiseFrom Telescope
gamma_phis Int
0

  caseMaybeM (expandRecordVar (raiseFrom gamma x) working_tel) __IMPOSSIBLE__ $ \ (Telescope
_,Substitution
tau,Substitution
rho,Telescope
_) -> do
    String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.build" Int
30 (TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ())
-> TCMT IO Doc -> ExceptT NoLeftInv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
working_tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau    :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
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
$ ((Telescope
working_tel,Substitution
rho,Substitution
tau,Int -> Substitution
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 Typeω"
-- 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 EtaExpandVar{}      = m Doc
"eta-expansion of variables"
explainStep EtaExpandEquation{} = m Doc
"eta-expansion of equations"
explainStep SkipIrrelevantEquation{} = m Doc
"ignoring irrelevant equations"