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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
  where
    unLevel :: Term -> m Term
unLevel (Level Level
l) = forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
    unLevel Term
u         = 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnifyState] -> ShowS
$cshowList :: [UnifyState] -> ShowS
show :: UnifyState -> String
$cshow :: UnifyState -> String
showsPrec :: Int -> UnifyState -> ShowS
$cshowsPrec :: Int -> 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) 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) 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' = 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
    [ m Doc
"variable tel:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
    , m Doc
"flexible vars: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. FlexibleVar a -> (a, IsForced)
flexVarF forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
state)
    , m Doc
"equation tel:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta)
    , m Doc
"equations:     " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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 = (forall a. FlexibleVar a -> a
flexVar FlexibleVar a
fi, 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 = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=?=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, 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) <- 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 = forall a. Sized a => a -> Int
size [Arg Term]
lhs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Arg Term]
rhs) forall a. HasCallStack => a
__IMPOSSIBLE__
  TelV Telescope
eqTel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Telescope
eqTel) forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
eqTel

varCount :: UnifyState -> Int
varCount :: UnifyState -> Int
varCount = forall a. Sized a => a -> Int
size 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 = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel 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 = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i

eqCount :: UnifyState -> Int
eqCount :: UnifyState -> Int
eqCount = forall a. Sized a => a -> Int
size 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 (forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
eqs) Int
k)
          (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
          (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault 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
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
eqTel UnifyState
s) (forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term Type
a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
eqs) Int
k)
          (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
          (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault 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
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Dom (String, Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
k forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) (forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term Type
a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 -> forall a. Maybe a
Nothing
  Just (Telescope
tel' , PatternSubstitution
sigma , Permutation
rho) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (,PatternSubstitution
sigma) 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) forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
s
      , eqTel :: Telescope
eqTel    = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      , eqLHS :: [Arg Term]
eqLHS    = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
      , eqRHS :: [Arg Term]
eqRHS    = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma 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 =
      forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a b. (a -> b) -> a -> b
$ \(FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p Int
x) ->
        forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. Ord a => a -> a -> Bool
< Int
0     = forall a. HasCallStack => a
__IMPOSSIBLE__
 | Int
k forall a. Eq a => a -> a -> Bool
== Int
0    = Telescope
tel forall t. Apply t => t -> Term -> t
`apply1` Term
u
 | Bool
otherwise = case Telescope
tel of
    Telescope
EmptyTel         -> forall a. HasCallStack => a
__IMPOSSIBLE__
    ExtendTel Dom' Term Type
a Abs Telescope
tel' -> forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
a forall a b. (a -> b) -> a -> b
$
      forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Telescope
tel') forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Term -> Telescope
applyUnder (Int
kforall a. Num a => a -> a -> a
-Int
1) (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
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__
dropAt Int
k (a
x:[a]
xs)
 | Int
k forall a. Ord a => a -> a -> Bool
< Int
0     = forall a. HasCallStack => a
__IMPOSSIBLE__
 | Int
k forall a. Eq a => a -> a -> Bool
== Int
0    = [a]
xs
 | Bool
otherwise = a
x forall a. a -> [a] -> [a]
: forall a. Int -> [a] -> [a]
dropAt (Int
kforall 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) 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    = forall a. Int -> [a] -> [a]
dropAt Int
k forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
    , eqRHS :: [Arg Term]
eqRHS    = forall a. Int -> [a] -> [a]
dropAt Int
k forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
    }
  where
    u' :: Term
u'    = forall a. Subst a => Int -> a -> a
raise Int
k Term
u
    n :: Int
n     = UnifyState -> Int
eqCount UnifyState
s
    sigma :: PatternSubstitution
sigma = forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nforall a. Num a => a -> a -> a
-Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (forall a. Term -> Pattern' a
dotP Term
u') 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnifyStep] -> ShowS
$cshowList :: [UnifyStep] -> ShowS
show :: UnifyStep -> String
$cshow :: UnifyStep -> String
showsPrec :: Int -> UnifyStep -> ShowS
$cshowsPrec :: Int -> 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , m Doc
"lhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ])
    Solution Int
k Dom' Term Type
a FlexibleVar Int
i Term
u Either () ()
s -> m Doc
"Solution" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom' Term Type
a
      , m Doc
"variable:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show (forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
i, forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
i, forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
i, forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
i))
      , m Doc
"term:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , m Doc
"side:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Either () ()
s)
      ])
    Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c -> m Doc
"Injectivity" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
      , m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"indices:    " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
ixs)
      , m Doc
"constructor:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
      ])
    Conflict Int
k Type
a QName
d [Arg Term]
pars Term
u Term
v -> m Doc
"Conflict" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
      , m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"lhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ])
    Cycle Int
k Type
a QName
d [Arg Term]
pars Int
i Term
u -> m Doc
"Cycle" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , m Doc
"datatype:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
      , m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
      , m Doc
"variable:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
i)
      , m Doc
"term:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      ])
    EtaExpandVar FlexibleVar Int
fi QName
r [Arg Term]
pars -> m Doc
"EtaExpandVar" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"variable:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show FlexibleVar Int
fi)
      , m Doc
"record type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
      , m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars
      ])
    EtaExpandEquation Int
k QName
r [Arg Term]
pars -> m Doc
"EtaExpandEquation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"record type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
      , m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars
      ])
    LitConflict Int
k Type
a Literal
u Literal
v -> m Doc
"LitConflict" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , m Doc
"lhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
u
      , m Doc
"rhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
v
      ])
    StripSizeSuc Int
k Term
u Term
v -> m Doc
"StripSizeSuc" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"lhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , m Doc
"rhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ])
    SkipIrrelevantEquation Int
k -> m Doc
"SkipIrrelevantEquation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      ])
    TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs -> m Doc
"TypeConInjectivity" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ m Doc
"position:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
      , m Doc
"datatype:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
      , m Doc
"lhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
us)
      , m Doc
"rhs:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
x
    , unifyProof :: PatternSubstitution
unifyProof = UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
y 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 forall a. Substitution' a
IdS forall a. Substitution' a
IdS -- []
  mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
mappend = 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
sub forall a. Substitution' a
IdS

tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifyProof :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sub = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (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 = forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT UnifyLogT m a
m