{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.LHS.Unify.LeftInverse where

import Prelude hiding ((!!), null)

import Control.Monad
import Control.Monad.State
import Control.Monad.Writer (WriterT(..), MonadWriter(..))
import Control.Monad.Except

import Data.Semigroup hiding (Arg)
import qualified Data.List as List
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)

import qualified Agda.Benchmarking as Bench

import Agda.Interaction.Options (optInjectiveTypeConstructors, optCubical, optWithoutK)

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

import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Builtin -- (constructorForm, getTerm, builtinPathP)
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Primitive.Cubical
import Agda.TypeChecking.Names
import Agda.TypeChecking.Conversion -- equalTerm
import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Patterns.Match as Match
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Records

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

import Agda.Utils.Empty
import Agda.Utils.Either
import Agda.Utils.Benchmark
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.WithDefault
import Agda.Utils.Tuple

import Agda.Utils.Impossible

instance PrettyTCM NoLeftInv where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NoLeftInv -> m Doc
prettyTCM (UnsupportedYet UnifyStep
s) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"It relies on" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
explainStep UnifyStep
s forall a. Semigroup a => a -> a -> a
<> m Doc
","] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is not yet supported"
  prettyTCM NoLeftInv
UnsupportedCxt     = forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"it relies on higher-dimensional unification, which is not yet supported"
  prettyTCM (Illegal UnifyStep
s)        = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"It relies on" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
explainStep UnifyStep
s forall a. Semigroup a => a -> a -> a
<> m Doc
","] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is incompatible with" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cubical Agda"]
  prettyTCM NoLeftInv
NoCubical          = forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Cubical Agda is disabled"
  prettyTCM NoLeftInv
WithKEnabled       = forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"The K rule is enabled"
  prettyTCM NoLeftInv
SplitOnStrict      = forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"It splits on a type in SSet"
  prettyTCM NoLeftInv
SplitOnFlat        = 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NoLeftInv] -> ShowS
$cshowList :: [NoLeftInv] -> ShowS
show :: NoLeftInv -> String
$cshow :: NoLeftInv -> String
showsPrec :: Int -> NoLeftInv -> ShowS
$cshowsPrec :: Int -> 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
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 forall a b. (a -> b) -> a -> b
$ do
    Maybe Cubical
cubical <- PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    TCMT IO Doc
"cubical:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Maybe Cubical
cubical)
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 forall a b. (a -> b) -> a -> b
$ do
    Maybe Term
pathp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getTerm' String
builtinPathP
    TCMT IO Doc
"pathp:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust Maybe Term
pathp)
  let cond :: tcm Bool
cond = 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.
       [
         forall a. Null a => a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
       ]
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM tcm Bool
cond (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left NoLeftInv
UnsupportedCxt) forall a b. (a -> b) -> a -> b
$ do
  [Either NoLeftInv (Retract, Term)]
equivs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM UnifyLog
log forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyLogEntry
-> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
buildEquiv
  case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either NoLeftInv (Retract, Term)]
equivs of
    Left NoLeftInv
no -> do
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv.badstep" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"No Left Inverse:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (NoLeftInv -> UnifyStep
badStep NoLeftInv
no)
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Substitution' a
idS,forall a. Int -> Substitution' a
raiseS Int
1)
      [(Retract, Term)]
xs -> do
        let
            loop :: [(Retract, Term)] -> m Retract
loop [] = forall a. HasCallStack => a
__IMPOSSIBLE__
            loop [(Retract, Term)
x] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
              forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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) <- forall {m :: * -> *}.
(PureTCM m, MonadError TCErr m) =>
[(Retract, Term)] -> m Retract
loop [(Retract, Term)]
xs
        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 forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall a. Int -> Substitution' a
raiseS Int
1
    IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
    let replaceAt :: Int -> a -> [a] -> [a]
replaceAt Int
n a
x [a]
xs = [a]
xs0 forall a. [a] -> [a] -> [a]
++ a
xforall a. a -> [a] -> [a]
:[a]
xs1
                where ([a]
xs0,a
_:[a]
xs1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
xs
    let max :: Term -> Term -> Term
max Term
r Term
s = IntervalView -> Term
unview forall a b. (a -> b) -> a -> b
$ Arg Term -> Arg Term -> IntervalView
IMax (forall e. e -> Arg e
argN Term
r) (forall e. e -> Arg e
argN Term
s)
        neg :: Term -> Term
neg Term
r = IntervalView -> Term
unview forall a b. (a -> b) -> a -> b
$ Arg Term -> IntervalView
INeg (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 (forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s0) forall a. Num a => a -> a -> a
+ Int
1)
                       -- I + us =_Δ vs -- inplaceS
    let leftInv :: Substitution
leftInv = forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall {a}. Int -> a -> [a] -> [a]
replaceAt (forall a. Sized a => a -> Int
size (UnifyState -> Telescope
varTel UnifyState
s0)) Term
phieq forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution
leftInv0) forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom (forall a. Sized a => a -> Int
size (UnifyState -> Telescope
varTel UnifyState
s0) forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s0))
    let working_tel :: Telescope
working_tel = forall t. Abstract t => Telescope -> t -> t
abstract (UnifyState -> Telescope
varTel UnifyState
s0) (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel HasCallStack => Dom Type
__DUMMY_DOM__ forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs String
"phi0" forall a b. (a -> b) -> a -> b
$ (UnifyState -> Telescope
eqTel UnifyState
s0))
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=== before mod"
    do
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
working_tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau0    :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
tau0
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
working_tel forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"r" :: String, HasCallStack => Dom Type
__DUMMY_DOM__)
                               forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv0:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
leftInv0

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

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall a. [a] -> [a]
reverse [a]
xs forall a. DeBruijn a => [a] -> Substitution' a -> 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
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=== composing"
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Γ0   :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
prob0
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob0 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau0  :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
tau0
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Γ1   :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
prob1
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau1  :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
rho0
  let tau :: Substitution
tau = Substitution
tau0 forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
tau1

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

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

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

  Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  Term
max <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
  Term
neg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
  Right Abs [Term]
leftInv <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob0 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT (Telescope -> Names
teleNames Telescope
prob0) forall a b. (a -> b) -> a -> b
$ do
             NamesT tcm Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
phi0
             NamesT tcm Telescope
g0 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
prob0) Telescope
prob0
             NamesT tcm (Abs [Arg Term])
step0 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs String
"i" forall a b. (a -> b) -> a -> b
$ Substitution
step0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
prob0
             NamesT tcm (Abs [Term])
leftInv0 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs String
"i" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ Substitution
leftInv0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
prob0
             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 a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT tcm b
i -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"i" :: String, forall a. a -> Dom a
defaultDom Type
interval) forall a b. (a -> b) -> a -> b
$ do
              Abs Telescope
tel <- 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 a b. (a -> b) -> a -> b
$ \ (NamesT tcm Term
_ :: NamesT tcm Term) -> NamesT tcm Telescope
g0
              [Arg Term]
step0i <- forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT tcm (Abs [Arg Term])
step0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT tcm b
i
              Term
face <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
max forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
neg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b. (Subst b, DeBruijn b) => NamesT tcm b
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT tcm Term
phi
              Abs [Term]
leftInv0 <- NamesT tcm (Abs [Term])
leftInv0
              Term
i <- forall b. (Subst b, DeBruijn b) => NamesT tcm b
i
              -- this composition could be optimized further whenever step0i is actually constant in i.
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob0 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"r" :: String, HasCallStack => Dom Type
__DUMMY_DOM__) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv  :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv)
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob0 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"r" :: String, HasCallStack => Dom Type
__DUMMY_DOM__) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInv  :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Subst a => Abs a -> a
absBody Abs [Term]
leftInv)
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
prob0 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"r" :: String, HasCallStack => Dom Type
__DUMMY_DOM__) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"leftInvSub  :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> a
absBody forall a b. (a -> b) -> a -> b
$ Abs [Term]
leftInv)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
prob, Substitution
rho, Substitution
tau , forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
termsS forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> a
absBody 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 = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT 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 = 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
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"step unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
st
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"step step:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
st) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyStep
step)
        IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
        Telescope
cxt <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"context:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          v :: Arg Term
v = UnifyState -> [Arg Term]
eqRHS UnifyState
st forall a. HasCallStack => [a] -> Int -> a
!! Int
k
          x :: Int
x = forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fx
          neqs :: Int
neqs = forall a. Sized a => a -> Int
size Telescope
eqs
          phis :: Int
phis = Int
1 -- neqs
        Type
interval <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
         -- Γ, φs : I^phis
        let gamma_phis :: Telescope
gamma_phis = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma forall a b. (a -> b) -> a -> b
$ ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$
              forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Dom a
defaultDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Type
interval) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"phi" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [Int
0 .. Int
phis forall a. Num a => a -> a -> a
- Int
1]
        Telescope
working_tel <- forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma_phis forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported (forall (m :: * -> *).
(PureTCM m, MonadError (Closure Type) m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope' (forall a. Subst a => Int -> a -> a
raise Int
phis forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
st) (forall a. Subst a => Int -> a -> a
raise Int
phis forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
st) (forall a. Subst a => Int -> a -> a
raise Int
phis forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
st))
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"working tel:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope
working_tel :: Telescope)
          , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
working_tel forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"working tel args:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
working_tel :: [Arg Term])
          ]
        ([Arg Term]
tau,[Arg Term]
leftInv,Term
phi) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
working_tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
          let raiseFrom :: Telescope -> Term -> Term
raiseFrom Telescope
tel Term
x = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
working_tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Telescope
tel) Term
x

          [NamesT (ExceptT NoLeftInv tcm) Term
u,NamesT (ExceptT NoLeftInv tcm) Term
v] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> Term -> Term
raiseFrom Telescope
gamma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
u,Arg Term
v]
          -- φ
          let phi :: Term
phi = Telescope -> Term -> Term
raiseFrom Telescope
gamma_phis forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
          -- working_tel ⊢ γ₁,x,γ₂,φ,eqs
          let all_args :: [Arg Term]
all_args = 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,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) = forall {a}. (Telescope, a) -> (Telescope, AbsN a)
bindSplit forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt (forall a. Sized a => a -> Int
size Telescope
gamma forall a. Num a => a -> a -> a
- Int
x forall a. Num a => a -> a -> a
- Int
1) Telescope
working_tel
          let ([Arg Term]
gamma1_args,[Arg Term]
xxi_args) = forall a. Int -> [a] -> ([a], [a])
splitAt (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) = forall a. Int -> [a] -> ([a], [a])
splitAt ((forall a. Sized a => a -> Int
size Telescope
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Telescope
gamma1) forall a. Num a => a -> a -> a
+ Int
phis 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 = forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN Telescope
xxi forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Term]
gamma1_args
          --                                                      x:A,Γ₂                φ
          let (Telescope
xpre,AbsN Telescope
krest) = forall {a}. (Telescope, a) -> (Telescope, AbsN a)
bindSplit forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt ((forall a. Sized a => a -> Int
size Telescope
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Telescope
gamma1) forall a. Num a => a -> a -> a
+ Int
phis forall a. Num a => a -> a -> a
+ Int
k) Telescope
xxi_here
          NamesT (ExceptT NoLeftInv tcm) Term
k_arg <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
k_arg
          NamesT (ExceptT NoLeftInv tcm) Telescope
xpre <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Telescope
xpre
          NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
krest <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open AbsN Telescope
krest
          AbsN Telescope
delta <- forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN [String
"x",String
"eq"] 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 = forall t. Apply t => t -> Term -> t
apply1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Telescope
xpre forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
x
                     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 a b. (a -> b) -> a -> b
$ \ Vars (ExceptT NoLeftInv tcm)
args ->
                       forall t. Apply t => t -> Term -> t
apply1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
xforall a. a -> [a] -> [a]
:Vars (ExceptT NoLeftInv tcm)
args) 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 forall a. [a] -> [a] -> [a]
++ [Arg Term]
xi1
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size delta:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size forall a b. (a -> b) -> a -> b
$ forall a. AbsN a -> a
unAbsN AbsN Telescope
delta)
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size d0args:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size [Arg Term]
d_zero_args)
          let appSide :: Term -> Term
appSide = case Either () ()
side of
                          Left{} -> forall a. a -> a
id
                          Right{} -> IntervalView -> Term
unview forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> IntervalView
INeg forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e. e -> Arg e
defaultArg) 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Term
i)
                              , forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"j" 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 (forall e. e -> Arg e
argN Term
j) (forall e. e -> Arg e
argN Term
i))
                                            Right{} -> IntervalView -> Term
unview (Arg Term -> Arg Term -> IntervalView
IMin (forall e. e -> Arg e
argN Term
j) (forall e. e -> Arg e
argN forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntervalView -> Term
unview forall a b. (a -> b) -> a -> b
$ Arg Term -> IntervalView
INeg forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN Term
i))
                                  in NamesT (ExceptT NoLeftInv tcm) Term
k_arg 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Term
i 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 forall a. [a] -> [a] -> [a]
++ a
xforall a. a -> [a] -> [a]
:[a]
xs1
                where ([a]
xs0,a
_:[a]
xs1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
xs
              dropAt :: Int -> [a] -> [a]
dropAt Int
n [a]
xs = [a]
xs0 forall a. [a] -> [a] -> [a]
++ [a]
xs1
                where ([a]
xs0,a
_:[a]
xs1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
xs
          NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
delta <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open AbsN Telescope
delta
          Abs Telescope
d <- 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 a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
i -> 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' 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 forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                                   forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
errorToUnsupported (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))
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau    :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a b. (a -> b) -> [a] -> [b]
map (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 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
gamma1_args
            NamesT (ExceptT NoLeftInv tcm) Term
phi <- 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 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
xi0
            NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi1 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Arg Term]
xi1
            Abs Telescope
delta0 <- 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 a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
i -> forall t. Apply t => t -> [Arg Term] -> t
apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) Telescope
xpre forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Int -> [a] -> [a]
take Int
1 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 forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
i)
            NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta0 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs Telescope
delta0
            Abs [Arg Term]
xi0f <- 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 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 <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
delta0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) Term
phi forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
xi0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
i
                                 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (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 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs [Arg Term]
xi0f

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

        forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar (Telescope -> Int -> Int
raiseFrom Telescope
gamma Int
x) Telescope
working_tel) forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ (Telescope
_,Substitution
tau,Substitution
rho,Telescope
_) -> do
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
working_tel forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tau    :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
tau
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ((Telescope
working_tel,Substitution
rho,Substitution
tau,forall a. Int -> Substitution' a
raiseS Int
1),Term
phi)

buildEquiv (UnificationStep UnifyState
st UnifyStep
step UnifyOutput
output) UnifyState
_ = do
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.inv" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"steps"
  let illegal :: tcm (Either NoLeftInv (Retract, Term))
illegal     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ UnifyStep -> NoLeftInv
Illegal UnifyStep
step
      unsupported :: tcm (Either NoLeftInv (Retract, Term))
unsupported = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left 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{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    LitConflict{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Cycle{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
    UnifyStep
_ -> tcm (Either NoLeftInv (Retract, Term))
unsupported

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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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"