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

import Prelude hiding (null)

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

import Data.Foldable (toList)
import Data.Semigroup hiding (Arg)
import Data.DList (DList)
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.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

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

data Equality = Equal
  { Equality -> Dom' Term 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' Term Type
a Term
u Term
v) = Dom' Term Type -> Term -> Term -> Equality
Equal Dom' Term 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' Term Type
a Term
u Term
v) = Dom' Term Type -> Term -> Term -> Equality
Equal Dom' Term 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 -> Telescope
varTel   :: Telescope     -- ^ Don't reduce!
  , UnifyState -> FlexibleVars
flexVars :: FlexibleVars
  , UnifyState -> Telescope
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' Telescope UnifyState
lensVarTel :: Lens' Telescope UnifyState
lensVarTel   Telescope -> f Telescope
f UnifyState
s = Telescope -> f Telescope
f (UnifyState -> Telescope
varTel UnifyState
s) f Telescope -> (Telescope -> UnifyState) -> f UnifyState
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Telescope
tel -> UnifyState
s { varTel :: Telescope
varTel = Telescope
tel }
--UNUSED Liang-Ting Chen 2019-07-16
--lensFlexVars :: Lens' FlexibleVars UnifyState
--lensFlexVars f s = f (flexVars s) <&> \ flex -> s { flexVars = flex }

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

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

--UNUSED Liang-Ting Chen 2019-07-16
--lensEqRHS    :: Lens' Args UnifyState
--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
<+> Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
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
<+> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta)
    , m Doc
"equations:     " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma ([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 :: Telescope
gamma = UnifyState -> Telescope
varTel UnifyState
state
      delta :: Telescope
delta = UnifyState -> Telescope
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 =>
Telescope
-> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a [Arg Term]
lhs [Arg Term]
rhs = do
  (Telescope
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs) <- (Telescope, Type, [Arg Term], [Arg Term])
-> m (Telescope, Type, [Arg Term], [Arg Term])
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Telescope
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs)
  let n :: Int
n = [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
lhs
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
rhs) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  TelV Telescope
eqTel Type
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  UnifyState -> m UnifyState
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope
-> FlexibleVars
-> Telescope
-> [Arg Term]
-> [Arg Term]
-> UnifyState
UState Telescope
tel FlexibleVars
flex Telescope
eqTel [Arg Term]
lhs [Arg Term]
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 = Telescope -> Bool
forall a. Null a => a -> Bool
null (Telescope -> Bool)
-> (UnifyState -> Telescope) -> UnifyState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
eqTel

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

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

getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised :: Int -> UnifyState -> Dom' Term Type
getVarTypeUnraised Int
i UnifyState
s = (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> Dom' Term (String, Type) -> Dom' Term 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__ (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> [Dom' Term (String, Type)])
-> Telescope -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i

eqCount :: UnifyState -> Int
eqCount :: UnifyState -> Int
eqCount = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int)
-> (UnifyState -> Telescope) -> UnifyState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
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 -> Telescope
eqTel = Telescope
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
    Dom' Term Type -> Term -> Term -> Equality
Equal (Dom' Term Type -> [Dom' Term Type] -> Int -> Dom' Term Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom' Term Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
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' Term Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  Telescope -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
    (Dom' Term Type -> Term -> Term -> Equality)
-> m (Dom' Term Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
eqTel UnifyState
s) (Dom' Term Type -> m (Dom' Term Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term 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 -> Telescope
eqTel = Telescope
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
    Dom' Term Type -> Term -> Term -> Equality
Equal ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> Dom' Term (String, Type) -> Dom' Term 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__ (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
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' Term Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s
  Telescope -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
    (Dom' Term Type -> Term -> Term -> Equality)
-> m (Dom' Term Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext ([Dom' Term (String, Type)] -> Telescope
telFromList ([Dom' Term (String, Type)] -> Telescope)
-> [Dom' Term (String, Type)] -> Telescope
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
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> [Dom' Term (String, Type)])
-> Telescope -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) (Dom' Term Type -> m (Dom' Term Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term 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 with the given value.
--   Returns Nothing if there is a cycle.
solveVar :: Int             -- ^ Index @k@
         -> DeBruijnPattern -- ^ Solution @u@
         -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
solveVar :: Int
-> Pattern' DBPatVar
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution)
solveVar Int
k Pattern' DBPatVar
u UnifyState
s = case Telescope
-> Int
-> Pattern' DBPatVar
-> Maybe (Telescope, PatternSubstitution, Permutation)
instantiateTelescope (UnifyState -> Telescope
varTel UnifyState
s) Int
k Pattern' DBPatVar
u of
  Maybe (Telescope, PatternSubstitution, Permutation)
Nothing -> Maybe (UnifyState, PatternSubstitution)
forall a. Maybe a
Nothing
  Just (Telescope
tel' , PatternSubstitution
sigma , Permutation
rho) -> (UnifyState, PatternSubstitution)
-> Maybe (UnifyState, PatternSubstitution)
forall a. a -> Maybe a
Just ((UnifyState, PatternSubstitution)
 -> Maybe (UnifyState, PatternSubstitution))
-> (UnifyState, PatternSubstitution)
-> Maybe (UnifyState, PatternSubstitution)
forall a b. (a -> b) -> a -> b
$ (,PatternSubstitution
sigma) (UnifyState -> (UnifyState, PatternSubstitution))
-> UnifyState -> (UnifyState, PatternSubstitution)
forall a b. (a -> b) -> a -> b
$ UState
      { varTel :: Telescope
varTel   = Telescope
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 :: Telescope
eqTel    = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
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 ((FlexibleVar Int -> Maybe (FlexibleVar Int))
 -> FlexibleVars -> FlexibleVars)
-> (FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars
-> FlexibleVars
forall a b. (a -> b) -> a -> b
$ \(FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p Int
x) ->
        ArgInfo
-> IsForced
-> FlexibleVarKind
-> Maybe Int
-> Int
-> FlexibleVar Int
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p (Int -> FlexibleVar Int) -> Maybe Int -> Maybe (FlexibleVar Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x (Permutation -> [Int]
permPicks Permutation
perm)

applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder Int
k Telescope
tel Term
u
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
 | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Telescope
tel Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
`apply1` Term
u
 | Bool
otherwise = case Telescope
tel of
    Telescope
EmptyTel         -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
    ExtendTel Dom' Term Type
a Abs Telescope
tel' -> Dom' Term Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$
      String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Telescope -> String
forall a. Abs a -> String
absName Abs Telescope
tel') (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Term -> Telescope
applyUnder (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Abs Telescope -> Telescope
forall a. Subst a => Abs a -> a
absBody Abs Telescope
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 :: Telescope
eqTel    = Int -> Telescope -> Term -> Telescope
applyUnder Int
k (UnifyState -> Telescope
eqTel UnifyState
s) Term
u'
    , eqLHS :: [Arg Term]
eqLHS    = Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
dropAt Int
k ([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    = Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
dropAt Int
k ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
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' Term 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' Term 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' Term Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
prettyTCM Dom' Term 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[σ]
--  , unifyLog   :: UnifyLog
  }

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
--    , unifyLog   = unifyLog x ++ unifyLog y
    }

instance Monoid UnifyOutput where
  mempty :: UnifyOutput
mempty  = PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
forall a. Substitution' a
IdS PatternSubstitution
forall a. Substitution' a
IdS -- []
  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
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
sub PatternSubstitution
forall a. Substitution' a
IdS

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
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
forall a. Substitution' a
IdS PatternSubstitution
sub

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 :: Functor m => UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT :: forall (m :: * -> *) a.
Functor m =>
UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT UnifyLogT m a
m = (UnifyLog' -> UnifyLog) -> (a, UnifyLog') -> (a, UnifyLog)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd 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. WriterT w m a -> m (a, w)
runWriterT UnifyLogT m a
m