{-# OPTIONS_GHC -Wunused-imports #-}

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

import Prelude hiding (null)

import Control.Applicative ((<|>))
import Control.Monad

import Data.Foldable (toList)
import Data.DList (DList)

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.TypeChecking.Rules.LHS.Problem

import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.StrictWriter
import Agda.Utils.Impossible

----------------------------------------------------
-- Equalities
----------------------------------------------------

data Equality = Equal
  { Equality -> Dom Type
_eqType  :: Dom Type
  , Equality -> Term
_eqLeft  :: Term
  , Equality -> Term
_eqRight :: Term
  }

-- Jesper, 2020-01-19: The type type lives in the context of the
-- variables+equations, while the lhs/rhs only depend on the
-- variables, so there is no way to give a correct Reduce instance.
-- WRONG:
-- instance Reduce Equality where
--   reduce' (Equal a u v) = Equal <$> reduce' a <*> reduce' u <*> reduce' v

eqConstructorForm :: HasBuiltins m => Equality -> m Equality
eqConstructorForm :: forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm (Equal Dom Type
a Term
u Term
v) = Dom Type -> Term -> Term -> Equality
Equal Dom Type
a (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
u m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v

eqUnLevel :: (HasBuiltins m) => Equality -> m Equality
eqUnLevel :: forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equal Dom Type
a Term
u Term
v) = Dom Type -> Term -> Term -> Equality
Equal Dom Type
a (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
u m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
  where
    unLevel :: Term -> m Term
unLevel (Level Level
l) = Level -> m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
    unLevel Term
u         = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u

----------------------------------------------------
-- Unify state
----------------------------------------------------

data UnifyState = UState
  { UnifyState -> Tele (Dom Type)
varTel   :: Telescope     -- ^ Don't reduce!
  , UnifyState -> FlexibleVars
flexVars :: FlexibleVars
  , UnifyState -> Tele (Dom Type)
eqTel    :: Telescope     -- ^ Can be reduced eagerly.
  , UnifyState -> [Arg Term]
eqLHS    :: [Arg Term]    -- ^ Ends up in dot patterns (should not be reduced eagerly).
  , UnifyState -> [Arg Term]
eqRHS    :: [Arg Term]    -- ^ Ends up in dot patterns (should not be reduced eagerly).
  } deriving (Int -> UnifyState -> ShowS
[UnifyState] -> ShowS
UnifyState -> String
(Int -> UnifyState -> ShowS)
-> (UnifyState -> String)
-> ([UnifyState] -> ShowS)
-> Show UnifyState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyState -> ShowS
showsPrec :: Int -> UnifyState -> ShowS
$cshow :: UnifyState -> String
show :: UnifyState -> String
$cshowList :: [UnifyState] -> ShowS
showList :: [UnifyState] -> ShowS
Show)
-- Issues #3578 and #4125: avoid unnecessary reduction in unifier.

lensVarTel   :: Lens' UnifyState Telescope
lensVarTel :: Lens' UnifyState (Tele (Dom Type))
lensVarTel   Tele (Dom Type) -> f (Tele (Dom Type))
f UnifyState
s = Tele (Dom Type) -> f (Tele (Dom Type))
f (UnifyState -> Tele (Dom Type)
varTel UnifyState
s) f (Tele (Dom Type))
-> (Tele (Dom Type) -> UnifyState) -> f UnifyState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Tele (Dom Type)
tel -> UnifyState
s { varTel = tel }
{-# INLINE lensVarTel #-}
--UNUSED Liang-Ting Chen 2019-07-16
--lensFlexVars :: Lens' UnifyState FlexibleVars
--lensFlexVars f s = f (flexVars s) <&> \ flex -> s { flexVars = flex }

lensEqTel    :: Lens' UnifyState Telescope
lensEqTel :: Lens' UnifyState (Tele (Dom Type))
lensEqTel    Tele (Dom Type) -> f (Tele (Dom Type))
f UnifyState
s = Tele (Dom Type) -> f (Tele (Dom Type))
f (UnifyState -> Tele (Dom Type)
eqTel UnifyState
s) f (Tele (Dom Type))
-> (Tele (Dom Type) -> UnifyState) -> f UnifyState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Tele (Dom Type)
x -> UnifyState
s { eqTel = x }
{-# INLINE lensEqTel #-}

--UNUSED Liang-Ting Chen 2019-07-16
--lensEqLHS    :: Lens' UnifyState Args
--lensEqLHS    f s = f (eqLHS s) <&> \ x -> s { eqLHS = x }

--UNUSED Liang-Ting Chen 2019-07-16
--lensEqRHS    :: Lens' UnifyState Args
--lensEqRHS    f s = f (eqRHS s) <&> \ x -> s { eqRHS = x }

-- UNUSED Andreas, 2019-10-14
-- instance Reduce UnifyState where
--   reduce' (UState var flex eq lhs rhs) =
--     UState <$> reduce' var
--            <*> pure flex
--            <*> reduce' eq
--            <*> reduce' lhs
--            <*> reduce' rhs

-- Andreas, 2019-10-14, issues #3578 and #4125:
-- | Don't ever reduce the whole 'varTel', as it will destroy
-- readability of the context in interactive editing!
-- To make sure this insight is not lost, the following
-- dummy instance should prevent a proper 'Reduce' instance for 'UnifyState'.
instance Reduce UnifyState where
  reduce' :: UnifyState -> ReduceM UnifyState
reduce' = UnifyState -> ReduceM UnifyState
forall a. HasCallStack => a
__IMPOSSIBLE__

--UNUSED Liang-Ting Chen 2019-07-16
--reduceEqTel :: UnifyState -> TCM UnifyState
--reduceEqTel = lensEqTel reduce

-- UNUSED Andreas, 2019-10-14
-- instance Normalise UnifyState where
--   normalise' (UState var flex eq lhs rhs) =
--     UState <$> normalise' var
--            <*> pure flex
--            <*> normalise' eq
--            <*> normalise' lhs
--            <*> normalise' rhs

instance PrettyTCM UnifyState where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
state = m Doc
"UnifyState" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
    [ m Doc
"variable tel:  " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
gamma
    , m Doc
"flexible vars: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, IsForced)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow ((FlexibleVar Int -> (Int, IsForced))
-> FlexibleVars -> [(Int, IsForced)]
forall a b. (a -> b) -> [a] -> [b]
map FlexibleVar Int -> (Int, IsForced)
forall {a}. FlexibleVar a -> (a, IsForced)
flexVarF (FlexibleVars -> [(Int, IsForced)])
-> FlexibleVars -> [(Int, IsForced)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
state)
    , m Doc
"equation tel:  " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (Tele (Dom Type) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta)
    , m Doc
"equations:     " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> Arg Term -> m Doc)
-> [Arg Term] -> [Arg Term] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
forall {m :: * -> *} {a} {a}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
a -> a -> m Doc
prettyEquality (UnifyState -> [Arg Term]
eqLHS UnifyState
state) (UnifyState -> [Arg Term]
eqRHS UnifyState
state)))
    ])
    where
      flexVarF :: FlexibleVar a -> (a, IsForced)
flexVarF FlexibleVar a
fi = (FlexibleVar a -> a
forall a. FlexibleVar a -> a
flexVar FlexibleVar a
fi, FlexibleVar a -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar a
fi)
      gamma :: Tele (Dom Type)
gamma = UnifyState -> Tele (Dom Type)
varTel UnifyState
state
      delta :: Tele (Dom Type)
delta = UnifyState -> Tele (Dom Type)
eqTel UnifyState
state
      prettyEquality :: a -> a -> m Doc
prettyEquality a
x a
y = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=?=" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
y

initUnifyState
  :: PureTCM m
  => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
initUnifyState :: forall (m :: * -> *).
PureTCM m =>
Tele (Dom Type)
-> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
initUnifyState Tele (Dom Type)
tel FlexibleVars
flex Type
a [Arg Term]
lhs [Arg Term]
rhs = do
  (tel, a, lhs, rhs) <- (Tele (Dom Type), Type, [Arg Term], [Arg Term])
-> m (Tele (Dom Type), Type, [Arg Term], [Arg Term])
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Tele (Dom Type)
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs)
  let n = [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
lhs
  unless (n == size rhs) __IMPOSSIBLE__
  TelV eqTel _ <- telView a
  unless (n == size eqTel) __IMPOSSIBLE__
  return $ UState tel flex eqTel lhs rhs
  -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
  -- reduce $ UState tel flex eqTel lhs rhs

isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved = Tele (Dom Type) -> Bool
forall a. Null a => a -> Bool
null (Tele (Dom Type) -> Bool)
-> (UnifyState -> Tele (Dom Type)) -> UnifyState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Tele (Dom Type)
eqTel

varCount :: UnifyState -> Int
varCount :: UnifyState -> Int
varCount = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (Tele (Dom Type) -> Int)
-> (UnifyState -> Tele (Dom Type)) -> UnifyState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Tele (Dom Type)
varTel

-- | Get the type of the i'th variable in the given state
getVarType :: Int -> UnifyState -> Dom Type
getVarType :: Int -> UnifyState -> Dom Type
getVarType Int
i UnifyState
s = Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Tele (Dom Type) -> [Dom Type]) -> Tele (Dom Type) -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Tele (Dom Type)
varTel UnifyState
s) Int
i

getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised Int
i UnifyState
s = (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Tele (Dom Type) -> [Dom' Term (String, Type)])
-> Tele (Dom Type) -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Tele (Dom Type)
varTel UnifyState
s) Int
i

eqCount :: UnifyState -> Int
eqCount :: UnifyState -> Int
eqCount = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size (Tele (Dom Type) -> Int)
-> (UnifyState -> Tele (Dom Type)) -> UnifyState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Tele (Dom Type)
eqTel

-- | Get the k'th equality in the given state. The left- and right-hand sides
--   of the equality live in the varTel telescope, and the type of the equality
--   lives in the varTel++eqTel telescope
getEquality :: Int -> UnifyState -> Equality
getEquality :: Int -> UnifyState -> Equality
getEquality Int
k UState { eqTel :: UnifyState -> Tele (Dom Type)
eqTel = Tele (Dom Type)
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
    Dom Type -> Term -> Term -> Equality
Equal (Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
eqs) Int
k)
          (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
          (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)

getReducedEquality
  :: (MonadReduce m, MonadAddContext m)
  => Int -> UnifyState -> m Equality
getReducedEquality :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
k UnifyState
s = do
  let Equal Dom Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  Tele (Dom Type) -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (UnifyState -> Tele (Dom Type)
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom Type -> Term -> Term -> Equality
Equal
    (Dom Type -> Term -> Term -> Equality)
-> m (Dom Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type) -> m (Dom Type) -> m (Dom Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (UnifyState -> Tele (Dom Type)
eqTel UnifyState
s) (Dom Type -> m (Dom Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom Type
a)
    m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v

-- | As getEquality, but with the unraised type
getEqualityUnraised :: Int -> UnifyState -> Equality
getEqualityUnraised :: Int -> UnifyState -> Equality
getEqualityUnraised Int
k UState { eqTel :: UnifyState -> Tele (Dom Type)
eqTel = Tele (Dom Type)
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
    Dom Type -> Term -> Term -> Equality
Equal ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
eqs) Int
k)
          (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
          (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)

getReducedEqualityUnraised
  :: (MonadReduce m, MonadAddContext m)
  => Int -> UnifyState -> m Equality
getReducedEqualityUnraised :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s = do
  let Equal Dom Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s
  Tele (Dom Type) -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (UnifyState -> Tele (Dom Type)
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom Type -> Term -> Term -> Equality
Equal
    (Dom Type -> Term -> Term -> Equality)
-> m (Dom Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type) -> m (Dom Type) -> m (Dom Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext ([Dom' Term (String, Type)] -> Tele (Dom Type)
telFromList ([Dom' Term (String, Type)] -> Tele (Dom Type))
-> [Dom' Term (String, Type)] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a. Int -> [a] -> [a]
take Int
k ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
-> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Tele (Dom Type) -> [Dom' Term (String, Type)])
-> Tele (Dom Type) -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Tele (Dom Type)
eqTel UnifyState
s) (Dom Type -> m (Dom Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom Type
a)
    m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v

--UNUSED Liang-Ting Chen 2019-07-16
--getEqInfo :: Int -> UnifyState -> ArgInfo
--getEqInfo k UState { eqTel = eqs } =
--  domInfo $ indexWithDefault __IMPOSSIBLE__ (telToList eqs) k
--
---- | Add a list of equations to the front of the equation telescope
--addEqs :: Telescope -> [Arg Term] -> [Arg Term] -> UnifyState -> UnifyState
--addEqs tel us vs s =
--  s { eqTel = tel `abstract` eqTel s
--    , eqLHS = us ++ eqLHS s
--    , eqRHS = vs ++ eqRHS s
--    }
--  where k = size tel
--
--addEq :: Type -> Arg Term -> Arg Term -> UnifyState -> UnifyState
--addEq a u v = addEqs (ExtendTel (defaultDom a) (Abs underscore EmptyTel)) [u] [v]



-- | Instantiate the k'th variable (from the left) with the given value.
--   Returns Nothing if there is a cycle.
solveVar :: Int             -- ^ De Bruijn _level_ @k@
         -> DeBruijnPattern -- ^ Solution @u@
         -> UnifyState -> Maybe (UnifyState, PatternSubstitution, Permutation)
solveVar :: Int
-> Pattern' DBPatVar
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution, Permutation)
solveVar Int
k Pattern' DBPatVar
u UnifyState
s = case Tele (Dom Type)
-> Int
-> Pattern' DBPatVar
-> Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
instantiateTelescope (UnifyState -> Tele (Dom Type)
varTel UnifyState
s) Int
k Pattern' DBPatVar
u of
  Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
Nothing -> Maybe (UnifyState, PatternSubstitution, Permutation)
forall a. Maybe a
Nothing
  Just (Tele (Dom Type)
tel' , PatternSubstitution
sigma , Permutation
perm) ->
    let rho :: Permutation
rho = Int -> Permutation -> Permutation
deleteP Int
k Permutation
perm
    in (UnifyState, PatternSubstitution, Permutation)
-> Maybe (UnifyState, PatternSubstitution, Permutation)
forall a. a -> Maybe a
Just ((UnifyState, PatternSubstitution, Permutation)
 -> Maybe (UnifyState, PatternSubstitution, Permutation))
-> (UnifyState, PatternSubstitution, Permutation)
-> Maybe (UnifyState, PatternSubstitution, Permutation)
forall a b. (a -> b) -> a -> b
$ (, PatternSubstitution
sigma , Permutation
perm) (UnifyState -> (UnifyState, PatternSubstitution, Permutation))
-> UnifyState -> (UnifyState, PatternSubstitution, Permutation)
forall a b. (a -> b) -> a -> b
$ UState
      { varTel :: Tele (Dom Type)
varTel   = Tele (Dom Type)
tel'
      , flexVars :: FlexibleVars
flexVars = Permutation -> FlexibleVars -> FlexibleVars
permuteFlex (Permutation -> Permutation
reverseP Permutation
rho) (FlexibleVars -> FlexibleVars) -> FlexibleVars -> FlexibleVars
forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
s
      , eqTel :: Tele (Dom Type)
eqTel    = PatternSubstitution -> Tele (Dom Type) -> Tele (Dom Type)
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ UnifyState -> Tele (Dom Type)
eqTel UnifyState
s
      , eqLHS :: [Arg Term]
eqLHS    = PatternSubstitution -> [Arg Term] -> [Arg Term]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
      , eqRHS :: [Arg Term]
eqRHS    = PatternSubstitution -> [Arg Term] -> [Arg Term]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
      }
  where
    permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
    permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
permuteFlex Permutation
perm = (FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars -> FlexibleVars
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
traverse (Permutation -> Int -> Maybe Int
lookupRP Permutation
perm))

applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder :: Int -> Tele (Dom Type) -> Term -> Tele (Dom Type)
applyUnder Int
k Tele (Dom Type)
tel Term
u
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
 | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Tele (Dom Type)
tel Tele (Dom Type) -> Term -> Tele (Dom Type)
forall t. Apply t => t -> Term -> t
`apply1` Term
u
 | Bool
otherwise = case Tele (Dom Type)
tel of
    Tele (Dom Type)
EmptyTel         -> Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
    ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel' -> Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$
      String -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. String -> a -> Abs a
Abs (Abs (Tele (Dom Type)) -> String
forall a. Abs a -> String
absName Abs (Tele (Dom Type))
tel') (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int -> Tele (Dom Type) -> Term -> Tele (Dom Type)
applyUnder (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom Type))
tel') Term
u

dropAt :: Int -> [a] -> [a]
dropAt :: forall a. Int -> [a] -> [a]
dropAt Int
_ [] = [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
dropAt Int
k (a
x:[a]
xs)
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
 | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = [a]
xs
 | Bool
otherwise = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
dropAt (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [a]
xs

-- | Solve the k'th equation with the given value, which can depend on
--   regular variables but not on other equation variables.
solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k Term
u UnifyState
s = (,PatternSubstitution
sigma) (UnifyState -> (UnifyState, PatternSubstitution))
-> UnifyState -> (UnifyState, PatternSubstitution)
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel    = applyUnder k (eqTel s) u'
    , eqLHS    = dropAt k $ eqLHS s
    , eqRHS    = dropAt k $ eqRHS s
    }
  where
    u' :: Term
u'    = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
k Term
u
    n :: Int
n     = UnifyState -> Int
eqCount UnifyState
s
    sigma :: PatternSubstitution
sigma = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (Term -> Pattern' DBPatVar
forall a. Term -> Pattern' a
dotP Term
u') PatternSubstitution
forall a. Substitution' a
idS

--UNUSED Liang-Ting Chen 2019-07-16
---- | Simplify the k'th equation with the given value (which can depend on other
----   equation variables). Returns Nothing if there is a cycle.
--simplifyEq :: Int -> Term -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
--simplifyEq k u s = case instantiateTelescope (eqTel s) k u of
--  Nothing -> Nothing
--  Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState
--    { varTel   = varTel s
--    , flexVars = flexVars s
--    , eqTel    = tel'
--    , eqLHS    = permute rho $ eqLHS s
--    , eqRHS    = permute rho $ eqRHS s
--    }
--
----------------------------------------------------
-- Unification strategies
----------------------------------------------------

data UnifyStep
  = Deletion
    { UnifyStep -> Int
deleteAt           :: Int
    , UnifyStep -> Type
deleteType         :: Type
    , UnifyStep -> Term
deleteLeft         :: Term
    , UnifyStep -> Term
deleteRight        :: Term
    }
  | Solution
    { UnifyStep -> Int
solutionAt         :: Int
    , UnifyStep -> Dom Type
solutionType       :: Dom Type
    , UnifyStep -> FlexibleVar Int
solutionVar        :: FlexibleVar Int
    , UnifyStep -> Term
solutionTerm       :: Term
    , UnifyStep -> Either () ()
solutionSide       :: Either () ()
      -- ^ side of the equation where the variable is.
    }
  | Injectivity
    { UnifyStep -> Int
injectAt           :: Int
    , UnifyStep -> Type
injectType         :: Type
    , UnifyStep -> QName
injectDatatype     :: QName
    , UnifyStep -> [Arg Term]
injectParameters   :: Args
    , UnifyStep -> [Arg Term]
injectIndices      :: Args
    , UnifyStep -> ConHead
injectConstructor  :: ConHead
    }
  | Conflict
    { UnifyStep -> Int
conflictAt         :: Int
    , UnifyStep -> Type
conflictType       :: Type
    , UnifyStep -> QName
conflictDatatype   :: QName
    , UnifyStep -> [Arg Term]
conflictParameters :: Args
    , UnifyStep -> Term
conflictLeft       :: Term
    , UnifyStep -> Term
conflictRight      :: Term
    }
  | Cycle
    { UnifyStep -> Int
cycleAt            :: Int
    , UnifyStep -> Type
cycleType          :: Type
    , UnifyStep -> QName
cycleDatatype      :: QName
    , UnifyStep -> [Arg Term]
cycleParameters    :: Args
    , UnifyStep -> Int
cycleVar           :: Int
    , UnifyStep -> Term
cycleOccursIn      :: Term
    }
  | EtaExpandVar
    { UnifyStep -> FlexibleVar Int
expandVar           :: FlexibleVar Int
    , UnifyStep -> QName
expandVarRecordType :: QName
    , UnifyStep -> [Arg Term]
expandVarParameters :: Args
    }
  | EtaExpandEquation
    { UnifyStep -> Int
expandAt           :: Int
    , UnifyStep -> QName
expandRecordType   :: QName
    , UnifyStep -> [Arg Term]
expandParameters   :: Args
    }
  | LitConflict
    { UnifyStep -> Int
litConflictAt      :: Int
    , UnifyStep -> Type
litType            :: Type
    , UnifyStep -> Literal
litConflictLeft    :: Literal
    , UnifyStep -> Literal
litConflictRight   :: Literal
    }
  | StripSizeSuc
    { UnifyStep -> Int
stripAt            :: Int
    , UnifyStep -> Term
stripArgLeft       :: Term
    , UnifyStep -> Term
stripArgRight      :: Term
    }
  | SkipIrrelevantEquation
    { UnifyStep -> Int
skipIrrelevantAt   :: Int
    }
  | TypeConInjectivity
    { UnifyStep -> Int
typeConInjectAt    :: Int
    , UnifyStep -> QName
typeConstructor    :: QName
    , UnifyStep -> [Arg Term]
typeConArgsLeft    :: Args
    , UnifyStep -> [Arg Term]
typeConArgsRight   :: Args
    } deriving (Int -> UnifyStep -> ShowS
[UnifyStep] -> ShowS
UnifyStep -> String
(Int -> UnifyStep -> ShowS)
-> (UnifyStep -> String)
-> ([UnifyStep] -> ShowS)
-> Show UnifyStep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyStep -> ShowS
showsPrec :: Int -> UnifyStep -> ShowS
$cshow :: UnifyStep -> String
show :: UnifyStep -> String
$cshowList :: [UnifyStep] -> ShowS
showList :: [UnifyStep] -> ShowS
Show)

instance PrettyTCM UnifyStep where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM UnifyStep
step = case UnifyStep
step of
    Deletion Int
k Type
a Term
u Term
v -> m Doc
"Deletion" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , m Doc
"lhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ])
    Solution Int
k Dom Type
a FlexibleVar Int
i Term
u Either () ()
s -> m Doc
"Solution" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
      , m Doc
"variable:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Int, Maybe Int, IsForced, FlexibleVarKind) -> String
forall a. Show a => a -> String
show (FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
i, FlexibleVar Int -> Maybe Int
forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
i, FlexibleVar Int -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
i, FlexibleVar Int -> FlexibleVarKind
forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
i))
      , m Doc
"term:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , m Doc
"side:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Either () () -> String
forall a. Show a => a -> String
show Either () ()
s)
      ])
    Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c -> m Doc
"Injectivity" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " 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 QName
d
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"indices:    " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
ixs)
      , m Doc
"constructor:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
      ])
    Conflict Int
k Type
a QName
d [Arg Term]
pars Term
u Term
v -> m Doc
"Conflict" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " 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 QName
d
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"lhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ])
    Cycle Int
k Type
a QName
d [Arg Term]
pars Int
i Term
u -> m Doc
"Cycle" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " 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 QName
d
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"variable:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i)
      , m Doc
"term:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      ])
    EtaExpandVar FlexibleVar Int
fi QName
r [Arg Term]
pars -> m Doc
"EtaExpandVar" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"variable:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fi)
      , m Doc
"record type:" 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 QName
r
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
pars
      ])
    EtaExpandEquation Int
k QName
r [Arg Term]
pars -> m Doc
"EtaExpandEquation" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"record type:" 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 QName
r
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
pars
      ])
    LitConflict Int
k Type
a Literal
u Literal
v -> m Doc
"LitConflict" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , m Doc
"lhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
u
      , m Doc
"rhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
v
      ])
    StripSizeSuc Int
k Term
u Term
v -> m Doc
"StripSizeSuc" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"lhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ])
    SkipIrrelevantEquation Int
k -> m Doc
"SkipIrrelevantEquation" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      ])
    TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs -> m Doc
"TypeConInjectivity" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"datatype:   " 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 QName
d
      , m Doc
"lhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
us)
      , m Doc
"rhs:        " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
      ])


----------------------------------------------------
-- Unify Log and monad
----------------------------------------------------

data UnifyLogEntry
 -- = UnificationDone  UnifyState
  = UnificationStep UnifyState UnifyStep UnifyOutput

type UnifyLog = [(UnifyLogEntry,UnifyState)]

-- | This variant of 'UnifyLog' is used to ensure that 'tell' is not
-- expensive.
type UnifyLog' = DList (UnifyLogEntry, UnifyState)

-- Given varΓ ⊢ eqΓ, varΓ ⊢ us, vs : eqΓ
data UnifyOutput = UnifyOutput
  { UnifyOutput -> PatternSubstitution
unifySubst :: PatternSubstitution -- varΓ' ⊢ σ : varΓ
  , UnifyOutput -> PatternSubstitution
unifyProof :: PatternSubstitution -- varΓ',eqΓ' ⊢ ps : eqΓ[σ]
                                      -- varΓ', us' =_eqΓ' vs' ⊢ ap(ps) : us[σ] =_{eqΓ[σ]} vs[σ]
    -- For solution steps, the dependency-preserving reordering of varΓ generated
    -- by instantiateTelescope (used by LeftInverse). Works on de Bruijn levels.
  , UnifyOutput -> Maybe Permutation
unifySolutionPerm :: Maybe Permutation
  }

instance Semigroup UnifyOutput where
  UnifyOutput
x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
<> UnifyOutput
y = UnifyOutput
    { unifySubst :: PatternSubstitution
unifySubst = UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
x
    , unifyProof :: PatternSubstitution
unifyProof = UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
x
    , unifySolutionPerm :: Maybe Permutation
unifySolutionPerm = UnifyOutput -> Maybe Permutation
unifySolutionPerm UnifyOutput
x Maybe Permutation -> Maybe Permutation -> Maybe Permutation
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> UnifyOutput -> Maybe Permutation
unifySolutionPerm UnifyOutput
y
    }

instance Monoid UnifyOutput where
  mempty :: UnifyOutput
mempty  = PatternSubstitution
-> PatternSubstitution -> Maybe Permutation -> UnifyOutput
UnifyOutput PatternSubstitution
forall a. Substitution' a
IdS PatternSubstitution
forall a. Substitution' a
IdS Maybe Permutation
forall a. Maybe a
Nothing
  mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
mappend = UnifyOutput -> UnifyOutput -> UnifyOutput
forall a. Semigroup a => a -> a -> a
(<>)

type UnifyLogT m a = WriterT UnifyLog' m a

type UnifyStepT m a = WriterT UnifyOutput m a

tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifySubst :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
sub = UnifyOutput -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
forall a b. (a -> b) -> a -> b
$ UnifyOutput
forall a. Monoid a => a
mempty { unifySubst = sub }

tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifyProof :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sub = UnifyOutput -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
forall a b. (a -> b) -> a -> b
$ UnifyOutput
forall a. Monoid a => a
mempty { unifyProof = sub }

tellUnifySolutionPerm :: MonadWriter UnifyOutput m => Permutation -> m ()
tellUnifySolutionPerm :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Permutation -> m ()
tellUnifySolutionPerm Permutation
perm = UnifyOutput -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
forall a b. (a -> b) -> a -> b
$ UnifyOutput
forall a. Monoid a => a
mempty { unifySolutionPerm = Just perm }

writeUnifyLog ::
  MonadWriter UnifyLog' m => (UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog :: forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog (UnifyLogEntry, UnifyState)
x = UnifyLog' -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ((UnifyLogEntry, UnifyState) -> UnifyLog'
forall el coll. Singleton el coll => el -> coll
singleton (UnifyLogEntry, UnifyState)
x) -- UnifyOutput IdS IdS [x]

runUnifyLogT :: Monad m => UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT :: forall (m :: * -> *) a. Monad m => UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT UnifyLogT m a
m = (UnifyLog' -> UnifyLog) -> (a, UnifyLog') -> (a, UnifyLog)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second UnifyLog' -> UnifyLog
forall a. DList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ((a, UnifyLog') -> (a, UnifyLog))
-> m (a, UnifyLog') -> m (a, UnifyLog)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyLogT m a -> m (a, UnifyLog')
forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
WriterT w m a -> m (a, w)
runWriterT UnifyLogT m a
m