{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

import Prelude hiding ((!!), null)

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

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.Size

import Agda.Utils.Impossible

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"

data NoLeftInv
  = UnsupportedYet {NoLeftInv -> UnifyStep
badStep :: UnifyStep}
  | Illegal        {badStep :: UnifyStep}
  | NoCubical
  | WithKEnabled
  | SplitOnStrict  -- ^ splitting on a Strict Set.
  | SplitOnFlat    -- ^ splitting on a @♭ argument
  | UnsupportedCxt
  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

buildLeftInverse :: (PureTCM tcm, MonadError TCErr tcm) => UnifyState -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse :: forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyState
-> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse UnifyState
s0 UnifyLog
log = do
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
    Maybe Cubical
cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
    TCMT IO Doc
"cubical:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Maybe Cubical -> String
forall a. Show a => a -> String
show Maybe Cubical
cubical)
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
    Maybe Term
pathp <- BuiltinId -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' BuiltinId
builtinPathP
    TCMT IO Doc
"pathp:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Bool -> String
forall a. Show a => a -> String
show (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust Maybe Term
pathp)
  let cond :: tcm Bool
cond = [tcm Bool] -> tcm 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) -> tcm Context -> tcm Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
       ]
  tcm 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 tcm Bool
cond (Either NoLeftInv (Substitution, Substitution)
-> tcm (Either NoLeftInv (Substitution, Substitution))
forall a. a -> tcm 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
  [Either NoLeftInv (Retract, Term)]
equivs <- UnifyLog
-> ((UnifyLogEntry, UnifyState)
    -> tcm (Either NoLeftInv (Retract, Term)))
-> tcm [Either NoLeftInv (Retract, Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM UnifyLog
log (((UnifyLogEntry, UnifyState)
  -> tcm (Either NoLeftInv (Retract, Term)))
 -> tcm [Either NoLeftInv (Retract, Term)])
-> ((UnifyLogEntry, UnifyState)
    -> tcm (Either NoLeftInv (Retract, Term)))
-> tcm [Either NoLeftInv (Retract, Term)]
forall a b. (a -> b) -> a -> b
$ (UnifyLogEntry
 -> UnifyState -> tcm (Either NoLeftInv (Retract, Term)))
-> (UnifyLogEntry, UnifyState)
-> tcm (Either NoLeftInv (Retract, Term))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry UnifyLogEntry
-> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyLogEntry
-> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
buildEquiv
  case [Either NoLeftInv (Retract, Term)]
-> Either NoLeftInv [(Retract, Term)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Either NoLeftInv (Retract, Term)]
equivs of
    Left NoLeftInv
no -> do
      String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm 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 -> do
    -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
    -- Γ,φ,us =_Δ vs, i : I ⊢ leftInv0 : Γ,φ,us =_Δ vs
    -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,φ,refls][τ0] = IdS : Γ,φ,us =_Δ vs
    (Substitution
tau0,Substitution
leftInv0) <- case [(Retract, Term)]
xs of
      [] -> (Substitution, Substitution) -> tcm (Substitution, Substitution)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution
forall a. Substitution' a
idS,Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1)
      [(Retract, Term)]
xs -> do
        let
            loop :: [(Retract, Term)] -> m Retract
loop [] = m Retract
forall a. HasCallStack => a
__IMPOSSIBLE__
            loop [(Retract, Term)
x] = Retract -> m Retract
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Retract -> m Retract) -> Retract -> m Retract
forall a b. (a -> b) -> a -> b
$ (Retract, Term) -> Retract
forall a b. (a, b) -> a
fst (Retract, Term)
x
            loop ((Retract, Term)
x:[(Retract, Term)]
xs) = do
              Retract
r <- [(Retract, Term)] -> m Retract
loop [(Retract, Term)]
xs
              (Retract -> Term -> Retract -> m Retract)
-> (Retract, Term) -> Retract -> m Retract
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Retract -> Term -> Retract -> m Retract
forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm,
 HasBuiltins tcm, MonadAddContext tcm) =>
Retract -> Term -> Retract -> tcm Retract
composeRetract (Retract, Term)
x Retract
r
        (Telescope
_,Substitution
_,Substitution
tau,Substitution
leftInv) <- [(Retract, Term)] -> tcm Retract
forall {m :: * -> *}.
(PureTCM m, MonadError TCErr m) =>
[(Retract, Term)] -> m Retract
loop [(Retract, Term)]
xs
        (Substitution, Substitution) -> tcm (Substitution, Substitution)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution
tau,Substitution
leftInv)
    -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
    -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,1,refls][τ] = idS : Γ,φ,us =_Δ vs
    let tau :: Substitution
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
    IntervalView -> Term
unview <- tcm (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
    let replaceAt :: Int -> a -> [a] -> [a]
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 -> Term -> Term
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 -> Term
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
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)
                       -- I + us =_Δ vs -- inplaceS
    let leftInv :: Substitution
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))
    let working_tel :: Telescope
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
$ String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
"phi0" (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ (UnifyState -> Telescope
eqTel UnifyState
s0))
    String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=== before mod"
    do
        Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)
                               (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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

    String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=== after mod"
    do
        Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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
        Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)
                               (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
leftInv

    Either NoLeftInv (Substitution, Substitution)
-> tcm (Either NoLeftInv (Substitution, Substitution))
forall a. a -> tcm 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
$ (Substitution, Substitution)
-> Either NoLeftInv (Substitution, Substitution)
forall a b. b -> Either a b
Right (Substitution
tau,Substitution
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 :: (PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm,HasBuiltins tcm, MonadAddContext tcm) => Retract -> Term -> Retract -> tcm Retract
composeRetract :: forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm,
 HasBuiltins tcm, MonadAddContext tcm) =>
Retract -> Term -> Retract -> tcm Retract
composeRetract (Telescope
prob0,Substitution
rho0,Substitution
tau0,Substitution
leftInv0) Term
phi0 (Telescope
prob1,Substitution
rho1,Substitution
tau1,Substitution
leftInv1) = do
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=== composing"
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ 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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ 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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 prob :: Telescope
prob = Telescope
prob0
  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

  Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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

  Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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

  Type
interval <- tcm Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  Term
max <- tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
  Term
neg <- tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
  Right Abs [Term]
leftInv <- (Abs (Either (Closure (Abs Type)) [Term])
 -> Either (Closure (Abs Type)) (Abs [Term]))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Either (Closure (Abs Type)) (Abs [Term]))
forall a b. (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Abs (Either (Closure (Abs Type)) [Term])
-> Either (Closure (Abs Type)) (Abs [Term])
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
sequenceA (tcm (Abs (Either (Closure (Abs Type)) [Term]))
 -> tcm (Either (Closure (Abs Type)) (Abs [Term])))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Either (Closure (Abs Type)) (Abs [Term]))
forall a b. (a -> b) -> a -> b
$ Telescope
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
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 (tcm (Abs (Either (Closure (Abs Type)) [Term]))
 -> tcm (Abs (Either (Closure (Abs Type)) [Term])))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
forall a b. (a -> b) -> a -> b
$ Names
-> NamesT tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT (Telescope -> Names
teleNames Telescope
prob0) (NamesT tcm (Abs (Either (Closure (Abs Type)) [Term]))
 -> tcm (Abs (Either (Closure (Abs Type)) [Term])))
-> NamesT tcm (Abs (Either (Closure (Abs Type)) [Term]))
-> tcm (Abs (Either (Closure (Abs Type)) [Term]))
forall a b. (a -> b) -> a -> b
$ do
             NamesT tcm Term
phi <- Term -> NamesT tcm (NamesT tcm Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
phi0
             NamesT tcm Telescope
g0 <- Telescope -> NamesT tcm (NamesT tcm Telescope)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Telescope -> NamesT tcm (NamesT tcm Telescope))
-> Telescope -> NamesT tcm (NamesT tcm Telescope)
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
prob0) Telescope
prob0
             NamesT tcm (Abs [Arg Term])
step0 <- Abs [Arg Term] -> NamesT tcm (NamesT tcm (Abs [Arg Term]))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Abs [Arg Term] -> NamesT tcm (NamesT tcm (Abs [Arg Term])))
-> Abs [Arg Term] -> NamesT tcm (NamesT tcm (Abs [Arg Term]))
forall a b. (a -> b) -> a -> b
$ String -> [Arg Term] -> Abs [Arg Term]
forall a. String -> a -> Abs a
Abs String
"i" ([Arg Term] -> Abs [Arg Term]) -> [Arg Term] -> Abs [Arg Term]
forall a b. (a -> b) -> a -> b
$ Substitution
Substitution' (SubstArg [Arg Term])
step0 Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
prob0
             NamesT tcm (Abs [Term])
leftInv0 <- Abs [Term] -> NamesT tcm (NamesT tcm (Abs [Term]))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Abs [Term] -> NamesT tcm (NamesT tcm (Abs [Term])))
-> Abs [Term] -> NamesT tcm (NamesT tcm (Abs [Term]))
forall a b. (a -> b) -> a -> b
$ String -> [Term] -> Abs [Term]
forall a. String -> a -> Abs a
Abs String
"i" ([Term] -> Abs [Term]) -> [Term] -> Abs [Term]
forall a b. (a -> b) -> a -> b
$ (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] -> [Term]
forall a b. (a -> b) -> a -> b
$ Substitution
Substitution' (SubstArg [Arg Term])
leftInv0 Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
prob0
             String
-> ((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
    -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
-> NamesT tcm (Abs (Either (Closure (Abs Type)) [Term]))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
  -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
 -> NamesT tcm (Abs (Either (Closure (Abs Type)) [Term])))
-> ((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
    -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
-> NamesT tcm (Abs (Either (Closure (Abs Type)) [Term]))
forall a b. (a -> b) -> a -> b
$ \ forall {b}. (Subst b, DeBruijn b) => NamesT tcm b
i -> (String, Dom Type)
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"i" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
interval) (NamesT tcm (Either (Closure (Abs Type)) [Term])
 -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
forall a b. (a -> b) -> a -> b
$ do
              Abs Telescope
tel <- String
-> ((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
    -> NamesT tcm Telescope)
-> NamesT tcm (Abs Telescope)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"_" (((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
  -> NamesT tcm Telescope)
 -> NamesT tcm (Abs Telescope))
-> ((forall {b}. (Subst b, DeBruijn b) => NamesT tcm b)
    -> NamesT tcm Telescope)
-> NamesT tcm (Abs Telescope)
forall a b. (a -> b) -> a -> b
$ \ (NamesT tcm Term
_ :: NamesT tcm Term) -> NamesT tcm Telescope
g0
              [Arg Term]
step0i <- 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 tcm (Abs [Arg Term]) -> NamesT tcm (Term -> [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT tcm (Abs [Arg Term])
step0 NamesT tcm (Term -> [Arg Term])
-> NamesT tcm Term -> NamesT tcm [Arg Term]
forall a b. NamesT tcm (a -> b) -> NamesT tcm a -> NamesT tcm b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT tcm Term
forall {b}. (Subst b, DeBruijn b) => NamesT tcm b
i
              Term
face <- Term -> NamesT tcm Term
forall a. a -> NamesT tcm a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
max NamesT tcm Term -> NamesT tcm Term -> NamesT tcm Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Term -> NamesT tcm Term
forall a. a -> NamesT tcm a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
neg NamesT tcm Term -> NamesT tcm Term -> NamesT tcm Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT tcm Term
forall {b}. (Subst b, DeBruijn b) => NamesT tcm b
i) NamesT tcm Term -> NamesT tcm Term -> NamesT tcm Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT tcm Term
phi
              Abs [Term]
leftInv0 <- NamesT tcm (Abs [Term])
leftInv0
              Term
i <- NamesT tcm Term
forall {b}. (Subst b, DeBruijn b) => NamesT tcm b
i
              -- this composition could be optimized further whenever step0i is actually constant in i.
              tcm (Either (Closure (Abs Type)) [Term])
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (tcm (Either (Closure (Abs Type)) [Term])
 -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
-> tcm (Either (Closure (Abs Type)) [Term])
-> NamesT tcm (Either (Closure (Abs Type)) [Term])
forall a b. (a -> b) -> a -> b
$ ExceptT (Closure (Abs Type)) tcm [Term]
-> tcm (Either (Closure (Abs Type)) [Term])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ((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])
-> ExceptT (Closure (Abs Type)) tcm [Arg Term]
-> ExceptT (Closure (Abs Type)) tcm [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) tcm [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpSysTel' Bool
True Abs Telescope
tel [(Term
i, Abs [Term]
leftInv0)] Term
face [Arg Term]
step0i)
  Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$
    String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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)
  Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$
    String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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)
  Telescope -> tcm () -> tcm ()
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 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type) -> tcm () -> tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$
    String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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 (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] -> [Term]) -> Abs [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Abs [Term]
leftInv)
  Retract -> tcm Retract
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
prob, Substitution
rho, Substitution
tau , 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] -> [Term]) -> Abs [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Abs [Term]
leftInv)

buildEquiv :: forall tcm. (PureTCM tcm, MonadError TCErr tcm) => UnifyLogEntry -> UnifyState -> tcm (Either NoLeftInv (Retract,Term))
buildEquiv :: forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyLogEntry
-> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
buildEquiv (UnificationStep UnifyState
st step :: UnifyStep
step@(Solution Int
k Dom Type
ty FlexibleVar Int
fx Term
tm Either () ()
side) UnifyOutput
output) UnifyState
next = ExceptT NoLeftInv tcm (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT NoLeftInv tcm (Retract, Term)
 -> tcm (Either NoLeftInv (Retract, Term)))
-> ExceptT NoLeftInv tcm (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ do
        let
          errorToUnsupported :: ExceptT a tcm b -> ExceptT NoLeftInv tcm b
          errorToUnsupported :: forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported ExceptT a tcm b
m = (a -> NoLeftInv) -> ExceptT a tcm b -> ExceptT NoLeftInv tcm b
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT (\ a
_ -> UnifyStep -> NoLeftInv
UnsupportedYet UnifyStep
step) ExceptT a tcm b
m
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ 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
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ 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 (UnifyState -> Telescope
varTel UnifyState
st) (UnifyStep -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM UnifyStep
step)
        IntervalView -> Term
unview <- ExceptT NoLeftInv tcm (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
        Telescope
cxt <- ExceptT NoLeftInv tcm Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"context:" 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
cxt
        let
          -- k counds in eqs from the left
          m :: Int
m = UnifyState -> Int
varCount UnifyState
st
          gamma :: Telescope
gamma = UnifyState -> Telescope
varTel UnifyState
st
          eqs :: Telescope
eqs = UnifyState -> Telescope
eqTel UnifyState
st
          u :: Arg Term
u = UnifyState -> [Arg Term]
eqLHS UnifyState
st [Arg Term] -> Int -> Arg Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          v :: Arg Term
v = UnifyState -> [Arg Term]
eqRHS UnifyState
st [Arg Term] -> Int -> Arg Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          x :: Int
x = FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fx
          neqs :: Int
neqs = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqs
          phis :: Int
phis = Int
1 -- neqs
        Type
interval <- tcm Type -> ExceptT NoLeftInv tcm 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 (tcm Type -> ExceptT NoLeftInv tcm Type)
-> tcm Type -> ExceptT NoLeftInv tcm Type
forall a b. (a -> b) -> a -> b
$ tcm Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
         -- Γ, φs : I^phis
        let gamma_phis :: Telescope
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
$
              (Int -> Dom (String, Type)) -> [Int] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map ((String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom ((String, Type) -> Dom (String, Type))
-> (Int -> (String, Type)) -> Int -> Dom (String, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) (String -> (String, Type))
-> (Int -> String) -> Int -> (String, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"phi" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [Int
0 .. Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        Telescope
working_tel <- Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma_phis (Telescope -> Telescope)
-> ExceptT NoLeftInv tcm Telescope
-> ExceptT NoLeftInv tcm Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          ExceptT (Closure Type) tcm Telescope
-> ExceptT NoLeftInv tcm Telescope
forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported (Telescope
-> [Arg Term] -> [Arg Term] -> ExceptT (Closure Type) tcm Telescope
forall (m :: * -> *).
(PureTCM m, MonadError (Closure Type) m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope' (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
phis (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
st) (Int -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> a -> a
raise Int
phis ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
st) (Int -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> a -> a
raise Int
phis ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
st))
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
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
"working tel:" 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
working_tel :: Telescope)
          , 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
"working tel args:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM (Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
working_tel :: [Arg Term])
          ]
        ([Arg Term]
tau,[Arg Term]
leftInv,Term
phi) <- Telescope
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
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 (ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
 -> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term))
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
forall a b. (a -> b) -> a -> b
$ Names
-> NamesT (ExceptT NoLeftInv tcm) ([Arg Term], [Arg Term], Term)
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (ExceptT NoLeftInv tcm) ([Arg Term], [Arg Term], Term)
 -> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term))
-> NamesT (ExceptT NoLeftInv tcm) ([Arg Term], [Arg Term], Term)
-> ExceptT NoLeftInv tcm ([Arg Term], [Arg Term], Term)
forall a b. (a -> b) -> a -> b
$ do
          let raiseFrom :: Telescope -> Term -> Term
raiseFrom Telescope
tel Term
x = Int -> Term -> Term
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) Term
x

          [NamesT (ExceptT NoLeftInv tcm) Term
u,NamesT (ExceptT NoLeftInv tcm) Term
v] <- (Arg Term
 -> NamesT
      (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
-> [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) 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 tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term
 -> NamesT
      (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> Term -> Term
raiseFrom Telescope
gamma (Term -> Term) -> (Arg Term -> Term) -> Arg Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term
u,Arg Term
v]
          -- φ
          let phi :: Term
phi = Telescope -> Term -> Term
raiseFrom Telescope
gamma_phis (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
          -- working_tel ⊢ γ₁,x,γ₂,φ,eqs
          let all_args :: [Arg Term]
all_args = Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
working_tel
          -- Γ₁,x : A,Γ₂
--          gamma <- open $ raiseFrom EmptyTel gamma
          -- -- γ₁,x,γ₂,φ,eqs : W
          -- working_tel <- open $ raiseFrom EmptyTel working_tel

          -- eq_tel <- open $ raiseFrom gamma (eqTel st)

          -- [lhs,rhs] <- mapM (open . raiseFrom gamma) [eqLHS st,eqRHS st]
          let bindSplit :: (Telescope, a) -> (Telescope, AbsN a)
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)
          -- . ⊢ Γ₁  ,  γ₁. (x : A),Γ₂,φ : I,[lhs ≡ rhs]
          let (Telescope
gamma1, AbsN Telescope
xxi) = (Telescope, Telescope) -> (Telescope, AbsN Telescope)
forall {a}. (Telescope, a) -> (Telescope, AbsN a)
bindSplit ((Telescope, Telescope) -> (Telescope, AbsN Telescope))
-> (Telescope, Telescope) -> (Telescope, AbsN Telescope)
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Telescope
working_tel
          let ([Arg Term]
gamma1_args,[Arg Term]
xxi_args) = Int -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma1) [Arg Term]
all_args
              (Arg Term
_x_arg:[Arg Term]
xi_args) = [Arg Term]
xxi_args
              (Arg Term
x_arg:[Arg Term]
xi0,Arg Term
k_arg:[Arg Term]
xi1) = Int -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Int -> [a] -> ([a], [a])
splitAt ((Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) [Arg Term]
xxi_args
              -- W ⊢ (x : A),Γ₂,φ : I,[lhs ≡ rhs]
          let
            xxi_here :: Telescope
            xxi_here :: Telescope
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 -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
gamma1_args
          --                                                      x:A,Γ₂                φ
          let (Telescope
xpre,AbsN Telescope
krest) = (Telescope, Telescope) -> (Telescope, AbsN Telescope)
forall {a}. (Telescope, a) -> (Telescope, AbsN a)
bindSplit ((Telescope, Telescope) -> (Telescope, AbsN Telescope))
-> (Telescope, Telescope) -> (Telescope, AbsN Telescope)
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt ((Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) Telescope
xxi_here
          NamesT (ExceptT NoLeftInv tcm) Term
k_arg <- Term
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term
 -> NamesT
      (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
-> Term
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
k_arg
          NamesT (ExceptT NoLeftInv tcm) Telescope
xpre <- Telescope
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Telescope)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Telescope
xpre
          NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
krest <- AbsN Telescope
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open AbsN Telescope
krest
          AbsN Telescope
delta <- Names
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     [NamesT (ExceptT NoLeftInv tcm) b])
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN [String
"x",String
"eq"] (((forall {b}.
   (Subst b, DeBruijn b) =>
   [NamesT (ExceptT NoLeftInv tcm) b])
  -> NamesT (ExceptT NoLeftInv tcm) Telescope)
 -> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     [NamesT (ExceptT NoLeftInv tcm) b])
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
forall a b. (a -> b) -> a -> b
$ \ [NamesT (ExceptT NoLeftInv tcm) Term
x,NamesT (ExceptT NoLeftInv tcm) Term
eq] -> do
                     let pre :: NamesT (ExceptT NoLeftInv tcm) Telescope
pre = Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
apply1 (Telescope -> Term -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
-> NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Telescope
xpre NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
x
                     NamesT (ExceptT NoLeftInv tcm) Telescope
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     [NamesT (ExceptT NoLeftInv tcm) b])
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall (m :: * -> *) a.
(MonadFail m, Abstract a) =>
NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
abstractN NamesT (ExceptT NoLeftInv tcm) Telescope
pre (((forall {b}.
   (Subst b, DeBruijn b) =>
   [NamesT (ExceptT NoLeftInv tcm) b])
  -> NamesT (ExceptT NoLeftInv tcm) Telescope)
 -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     [NamesT (ExceptT NoLeftInv tcm) b])
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
[NamesT (ExceptT NoLeftInv tcm) b]
args ->
                       Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
apply1 (Telescope -> Term -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
-> NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
-> [NamesT (ExceptT NoLeftInv tcm) (SubstArg Telescope)]
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
krest (NamesT (ExceptT NoLeftInv tcm) Term
xNamesT (ExceptT NoLeftInv tcm) Term
-> [NamesT (ExceptT NoLeftInv tcm) Term]
-> [NamesT (ExceptT NoLeftInv tcm) Term]
forall a. a -> [a] -> [a]
:[NamesT (ExceptT NoLeftInv tcm) Term]
forall {b}.
(Subst b, DeBruijn b) =>
[NamesT (ExceptT NoLeftInv tcm) b]
args) NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
eq
--          let delta_zero = absAppN delta $ map unArg [x_arg,k_arg]
          let d_zero_args :: [Arg Term]
d_zero_args = [Arg Term]
xi0 [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Arg Term]
xi1
          String -> Int -> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ())
-> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size delta:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ AbsN Telescope -> Telescope
forall a. AbsN a -> a
unAbsN AbsN Telescope
delta)
          String -> Int -> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ())
-> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size d0args:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
d_zero_args)
          let appSide :: Term -> Term
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 tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
csingl NamesT (ExceptT NoLeftInv tcm) Term
i = (NamesT (ExceptT NoLeftInv tcm) Term
 -> NamesT (ExceptT NoLeftInv tcm) (Arg Term))
-> [NamesT (ExceptT NoLeftInv tcm) Term]
-> NamesT (ExceptT NoLeftInv tcm) [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 tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) (Arg Term)
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) 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 tcm) Term]
 -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> [NamesT (ExceptT NoLeftInv tcm) Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b. (a -> b) -> a -> b
$ NamesT (ExceptT NoLeftInv tcm) Term
-> [NamesT (ExceptT NoLeftInv tcm) Term]
csingl' NamesT (ExceptT NoLeftInv tcm) Term
i
                  -- csingl' :: NamesT tcm Term -> [NamesT tcm Term]
                  csingl' :: NamesT (ExceptT NoLeftInv tcm) Term
-> [NamesT (ExceptT NoLeftInv tcm) Term]
csingl' NamesT (ExceptT NoLeftInv tcm) Term
i = [ NamesT (ExceptT NoLeftInv tcm) Term
k_arg NamesT (ExceptT NoLeftInv tcm) Term
-> (NamesT (ExceptT NoLeftInv tcm) Term,
    NamesT (ExceptT NoLeftInv tcm) Term,
    NamesT (ExceptT NoLeftInv tcm) Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT (ExceptT NoLeftInv tcm) Term
u, NamesT (ExceptT NoLeftInv tcm) Term
v, Term -> Term
appSide (Term -> Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Term
i)
                              , String
-> (NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"j" ((NamesT (ExceptT NoLeftInv tcm) Term
  -> NamesT (ExceptT NoLeftInv tcm) Term)
 -> NamesT (ExceptT NoLeftInv tcm) Term)
-> (NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT NoLeftInv tcm) 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 tcm) Term
k_arg NamesT (ExceptT NoLeftInv tcm) Term
-> (NamesT (ExceptT NoLeftInv tcm) Term,
    NamesT (ExceptT NoLeftInv tcm) Term,
    NamesT (ExceptT NoLeftInv tcm) Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT (ExceptT NoLeftInv tcm) Term
u, NamesT (ExceptT NoLeftInv tcm) Term
v, Term -> Term -> Term
r (Term -> Term -> Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Term
i NamesT (ExceptT NoLeftInv tcm) (Term -> Term)
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Term
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
j)
                              ]
          let replaceAt :: Int -> a -> [a] -> [a]
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 -> [a] -> [a]
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
          NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
delta <- AbsN Telescope
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open AbsN Telescope
delta
          Abs Telescope
d <- String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) Telescope)
 -> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i -> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
-> [NamesT (ExceptT NoLeftInv tcm) (SubstArg Telescope)]
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
delta (NamesT (ExceptT NoLeftInv tcm) Term
-> [NamesT (ExceptT NoLeftInv tcm) Term]
csingl' NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) 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 the
          -- solver when checking if "t" depends on "x" to decide what
          -- to transp and what not to.
          let flag :: Bool
flag = Bool
True
                 {-   φ -}
          [Arg Term]
tau <- {-dropAt (size gamma - 1 + k) .-} ([Arg Term]
gamma1_args [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++) ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                                   ExceptT NoLeftInv tcm [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT (Closure (Abs Type)) tcm [Arg Term]
-> ExceptT NoLeftInv tcm [Arg Term]
forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported (Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) tcm [Arg Term]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpTel' Bool
flag Abs Telescope
d Term
phi [Arg Term]
d_zero_args))
          String -> Int -> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ())
-> TCMT IO Doc -> NamesT (ExceptT NoLeftInv tcm) ()
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
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM ((Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) [Arg Term]
tau)
          [Arg Term]
leftInv <- do
            NamesT (ExceptT NoLeftInv tcm) [Arg Term]
gamma1_args <- [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) [Arg Term])
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
gamma1_args
            NamesT (ExceptT NoLeftInv tcm) Term
phi <- Term
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
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

            NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi0 <- [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) [Arg Term])
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
xi0
            NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi1 <- [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) [Arg Term])
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
xi1
            Abs Telescope
delta0 <- String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) Telescope)
 -> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i -> Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
apply (Telescope -> [Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
-> NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Telescope
xpre NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
1 ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
csingl NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i)
            NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta0 <- Abs Telescope
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (Abs Telescope))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs Telescope
delta0
            Abs [Arg Term]
xi0f <- String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
 -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term]))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i -> do
                                 ExceptT (Closure (Abs Type)) tcm [Arg Term]
m <- Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) tcm [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)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
-> NamesT
     (ExceptT NoLeftInv tcm)
     (Term
      -> [Arg Term]
      -> Term
      -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta0 NamesT
  (ExceptT NoLeftInv tcm)
  (Term
   -> [Arg Term]
   -> Term
   -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT
     (ExceptT NoLeftInv tcm)
     ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
phi NamesT
  (ExceptT NoLeftInv tcm)
  ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm)
     (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi0 NamesT
  (ExceptT NoLeftInv tcm)
  (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT
     (ExceptT NoLeftInv tcm)
     (ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i
                                 ExceptT NoLeftInv tcm [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT (Closure (Abs Type)) tcm [Arg Term]
-> ExceptT NoLeftInv tcm [Arg Term]
forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported ExceptT (Closure (Abs Type)) tcm [Arg Term]
m)
            NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
xi0f <- Abs [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term]))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs [Arg Term]
xi0f

            Abs Telescope
delta1 <- String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) Telescope)
 -> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope)
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i -> do

                   [NamesT (ExceptT NoLeftInv tcm) Term]
args <- (Arg Term
 -> NamesT
      (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
-> [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) 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 tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term
 -> NamesT
      (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT
     (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) 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 tcm) [NamesT (ExceptT NoLeftInv tcm) Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) 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 tcm) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
xi0f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i)
                   Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
apply (Telescope -> [Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) Telescope
-> NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
-> [NamesT (ExceptT NoLeftInv tcm) (SubstArg Telescope)]
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
krest (Int
-> [NamesT (ExceptT NoLeftInv tcm) Term]
-> [NamesT (ExceptT NoLeftInv tcm) Term]
forall a. Int -> [a] -> [a]
take Int
1 (NamesT (ExceptT NoLeftInv tcm) Term
-> [NamesT (ExceptT NoLeftInv tcm) Term]
csingl' NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i) [NamesT (ExceptT NoLeftInv tcm) Term]
-> [NamesT (ExceptT NoLeftInv tcm) Term]
-> [NamesT (ExceptT NoLeftInv tcm) Term]
forall a. [a] -> [a] -> [a]
++ [NamesT (ExceptT NoLeftInv tcm) Term]
args) NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) Telescope
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop Int
1 ([Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
csingl NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i)
            NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta1 <- Abs Telescope
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (Abs Telescope))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs Telescope
delta1
            Abs [Arg Term]
xi1f <- String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
 -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term]))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i -> do
                                 ExceptT (Closure (Abs Type)) tcm [Arg Term]
m <- Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) tcm [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)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
-> NamesT
     (ExceptT NoLeftInv tcm)
     (Term
      -> [Arg Term]
      -> Term
      -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta1 NamesT
  (ExceptT NoLeftInv tcm)
  (Term
   -> [Arg Term]
   -> Term
   -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT
     (ExceptT NoLeftInv tcm)
     ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
phi NamesT
  (ExceptT NoLeftInv tcm)
  ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm)
     (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi1 NamesT
  (ExceptT NoLeftInv tcm)
  (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT
     (ExceptT NoLeftInv tcm)
     (ExceptT (Closure (Abs Type)) tcm [Arg Term])
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i
                                 ExceptT NoLeftInv tcm [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT (Closure (Abs Type)) tcm [Arg Term]
-> ExceptT NoLeftInv tcm [Arg Term]
forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported ExceptT (Closure (Abs Type)) tcm [Arg Term]
m)
            NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
xi1f <- Abs [Arg Term]
-> NamesT
     (ExceptT NoLeftInv tcm)
     (NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term]))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs [Arg Term]
xi1f
            (Abs [Arg Term] -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Abs [Arg Term] -> [Arg Term]
forall a. Subst a => Abs a -> a
absBody (NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
 -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b. (a -> b) -> a -> b
$ String
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
"i" (((forall {b}.
   (Subst b, DeBruijn b) =>
   NamesT (ExceptT NoLeftInv tcm) b)
  -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
 -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term]))
-> ((forall {b}.
     (Subst b, DeBruijn b) =>
     NamesT (ExceptT NoLeftInv tcm) b)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
forall a b. (a -> b) -> a -> b
$ \ forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) 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 tcm) Term
i = ExceptT NoLeftInv tcm Term -> NamesT (ExceptT NoLeftInv tcm) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl (tcm Term -> ExceptT NoLeftInv tcm 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 tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg) NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT NoLeftInv tcm) Term
forall {b}.
(Subst b, DeBruijn b) =>
NamesT (ExceptT NoLeftInv tcm) b
i'
--              replaceAt (size gamma + k) <$> (fmap defaultArg $ cl primIMax <@> phi <@> i) <*> do
              do
                NamesT (ExceptT NoLeftInv tcm) [Arg Term]
gamma1_args NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [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 tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
csingl NamesT (ExceptT NoLeftInv tcm) Term
i NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [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 tcm) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
xi0f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
i) NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [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 tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
(a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
csingl NamesT (ExceptT NoLeftInv tcm) Term
i NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
-> NamesT (ExceptT NoLeftInv tcm) [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 tcm) (Abs [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
xi1f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
-> NamesT (ExceptT NoLeftInv tcm) Term
-> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
forall a b.
NamesT (ExceptT NoLeftInv tcm) (a -> b)
-> NamesT (ExceptT NoLeftInv tcm) a
-> NamesT (ExceptT NoLeftInv tcm) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
i))))
          ([Arg Term], [Arg Term], Term)
-> NamesT (ExceptT NoLeftInv tcm) ([Arg Term], [Arg Term], Term)
forall a. a -> NamesT (ExceptT NoLeftInv tcm) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
tau,[Arg Term]
leftInv,Term
phi)
        Term
iz <- tcm Term -> ExceptT NoLeftInv tcm 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 (tcm Term -> ExceptT NoLeftInv tcm Term)
-> tcm Term -> ExceptT NoLeftInv tcm Term
forall a b. (a -> b) -> a -> b
$ tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
        Term
io <- tcm Term -> ExceptT NoLeftInv tcm 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 (tcm Term -> ExceptT NoLeftInv tcm Term)
-> tcm Term -> ExceptT NoLeftInv tcm Term
forall a b. (a -> b) -> a -> b
$ tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
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
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM ((Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) [Arg Term]
tau)
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tauS   :" 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 (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
$ (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]
tau)
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type)
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"r" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
interval)
                               (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
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
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM ((Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) [Arg Term]
leftInv)
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv[0]:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM ([Arg Term] -> TCMT IO Doc) -> TCMT IO [Arg Term] -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Arg Term] -> TCMT IO [Arg Term]
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Int -> SubstArg [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg [Arg Term]
iz ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) [Arg Term]
leftInv))
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv[1]:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM ([Arg Term] -> TCMT IO Doc) -> TCMT IO [Arg Term] -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Arg Term] -> TCMT IO [Arg Term]
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce  (Int -> SubstArg [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg [Arg Term]
io ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) [Arg Term]
leftInv))
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
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 (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"[rho]tau :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                                                                                  -- k   φ
          Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM (Substitution' (SubstArg Substitution)
-> Substitution -> Substitution
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible
-> [SubstArg Substitution] -> Substitution' (SubstArg Substitution)
forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ ([SubstArg Substitution] -> Substitution' (SubstArg Substitution))
-> [SubstArg Substitution] -> Substitution' (SubstArg Substitution)
forall a b. (a -> b) -> a -> b
$ (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]
tau) (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Substitution
fromPatternSubstitution
                                                                      (PatternSubstitution -> Substitution)
-> PatternSubstitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Int -> PatternSubstitution -> PatternSubstitution
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
st) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1{-k-} Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
phis {-neqs{-φs-} - 1{-φ0-}-})
                                                                      (PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output)
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"."
        let rho0 :: Substitution
rho0 = PatternSubstitution -> Substitution
fromPatternSubstitution (PatternSubstitution -> Substitution)
-> PatternSubstitution -> Substitution
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
eqTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"prf :" 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 (PatternSubstitution -> Substitution
fromPatternSubstitution (PatternSubstitution -> Substitution)
-> PatternSubstitution -> Substitution
forall a b. (a -> b) -> a -> b
$ UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
output)
        let c0 :: Term
c0 = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"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)
        let c :: Term
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
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type)
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"φ" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
1 (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$
          String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"c :" 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 Term
c
--        let rho = liftS (neqs - k - 1) $ consS (raise (1 + k) c) $ liftS (1 + k) rho0
        let rho :: Substitution
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
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"old_sizes: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Int, Int) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
st, Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
st)
        String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"new_sizes: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Int, Int) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
next, 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)
--        addContext (abstract (varTel next) $ ExtendTel __DUMMY_DOM__ (Abs "φ" $ raise 1 $ eqTel next)) $
        Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ (String, Dom Type)
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"φ" :: String, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ Telescope -> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
1 (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
next) (ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ())
-> ExceptT NoLeftInv tcm () -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$
          String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
-> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rho   :" 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
rho
        (Retract, Term) -> ExceptT NoLeftInv tcm (Retract, Term)
forall a. a -> ExceptT NoLeftInv tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Retract, Term) -> ExceptT NoLeftInv tcm (Retract, Term))
-> (Retract, Term) -> ExceptT NoLeftInv tcm (Retract, Term)
forall a b. (a -> b) -> a -> b
$ ((Telescope
working_tel
                 , Substitution
rho
                 , 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
$ (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]
tau
                 , 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
$ (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]
leftInv)
                 , Term
phi)
buildEquiv (UnificationStep UnifyState
st step :: UnifyStep
step@(EtaExpandVar FlexibleVar Int
fv QName
_d [Arg Term]
_args) UnifyOutput
output) UnifyState
next = ((Retract, Term) -> Either NoLeftInv (Retract, Term))
-> tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Retract, Term) -> Either NoLeftInv (Retract, Term)
forall a b. b -> Either a b
Right (tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term)))
-> tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ do
        String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 TCMT IO Doc
"buildEquiv EtaExpandVar"
        let
          gamma :: Telescope
gamma = UnifyState -> Telescope
varTel UnifyState
st
          eqs :: Telescope
eqs = UnifyState -> Telescope
eqTel UnifyState
st
          x :: Int
x = FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fv
          neqs :: Int
neqs = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqs
          phis :: Int
phis = Int
1
        Type
interval <- tcm Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
         -- Γ, φs : I^phis
        let gamma_phis :: Telescope
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
$
              (Int -> Dom (String, Type)) -> [Int] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map ((String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom ((String, Type) -> Dom (String, Type))
-> (Int -> (String, Type)) -> Int -> Dom (String, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) (String -> (String, Type))
-> (Int -> String) -> Int -> (String, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"phi" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [Int
0 .. Int
phis Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        Telescope
working_tel <- Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma_phis (Telescope -> Telescope) -> tcm Telescope -> tcm Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Telescope -> [Arg Term] -> [Arg Term] -> tcm Telescope
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
phis (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
st) (Int -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> a -> a
raise Int
phis ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
st) (Int -> [Arg Term] -> [Arg Term]
forall a. Subst a => Int -> a -> a
raise Int
phis ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
st)
        let raiseFrom :: Telescope -> Int -> Int
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 :: Term
phi = Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Int -> Int
raiseFrom Telescope
gamma_phis Int
0

        tcm (Maybe (Telescope, Substitution, Substitution, Telescope))
-> tcm (Retract, Term)
-> ((Telescope, Substitution, Substitution, Telescope)
    -> tcm (Retract, Term))
-> tcm (Retract, Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Int
-> Telescope
-> tcm (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar (Telescope -> Int -> Int
raiseFrom Telescope
gamma Int
x) Telescope
working_tel) tcm (Retract, Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ (((Telescope, Substitution, Substitution, Telescope)
  -> tcm (Retract, Term))
 -> tcm (Retract, Term))
-> ((Telescope, Substitution, Substitution, Telescope)
    -> tcm (Retract, Term))
-> tcm (Retract, Term)
forall a b. (a -> b) -> a -> b
$ \ (Telescope
_,Substitution
tau,Substitution
rho,Telescope
_) -> do
          String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
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) -> tcm (Retract, Term)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Retract, Term) -> tcm (Retract, Term))
-> (Retract, Term) -> tcm (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)

buildEquiv (UnificationStep UnifyState
st UnifyStep
step UnifyOutput
output) UnifyState
_ = do
  String -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"steps"
  let illegal :: tcm (Either NoLeftInv (Retract, Term))
illegal     = Either NoLeftInv (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NoLeftInv (Retract, Term)
 -> tcm (Either NoLeftInv (Retract, Term)))
-> Either NoLeftInv (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ NoLeftInv -> Either NoLeftInv (Retract, Term)
forall a b. a -> Either a b
Left (NoLeftInv -> Either NoLeftInv (Retract, Term))
-> NoLeftInv -> Either NoLeftInv (Retract, Term)
forall a b. (a -> b) -> a -> b
$ UnifyStep -> NoLeftInv
Illegal UnifyStep
step
      unsupported :: tcm (Either NoLeftInv (Retract, Term))
unsupported = Either NoLeftInv (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NoLeftInv (Retract, Term)
 -> tcm (Either NoLeftInv (Retract, Term)))
-> Either NoLeftInv (Retract, Term)
-> tcm (Either NoLeftInv (Retract, Term))
forall a b. (a -> b) -> a -> b
$ NoLeftInv -> Either NoLeftInv (Retract, Term)
forall a b. a -> Either a b
Left (NoLeftInv -> Either NoLeftInv (Retract, Term))
-> NoLeftInv -> Either NoLeftInv (Retract, Term)
forall a b. (a -> b) -> a -> b
$ UnifyStep -> NoLeftInv
UnsupportedYet UnifyStep
step
  case UnifyStep
step of
    Deletion{}           -> tcm (Either NoLeftInv (Retract, Term))
illegal
    TypeConInjectivity{} -> tcm (Either NoLeftInv (Retract, Term))
illegal
    -- These should end up in a NoUnify
    Conflict{}    -> tcm (Either NoLeftInv (Retract, Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    LitConflict{} -> tcm (Either NoLeftInv (Retract, Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    Cycle{}       -> tcm (Either NoLeftInv (Retract, Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    UnifyStep
_ -> tcm (Either NoLeftInv (Retract, Term))
unsupported

{-# 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"