{-# LANGUAGE NondecreasingIndentation   #-}
{-# LANGUAGE UndecidableInstances       #-}

-- | Unification algorithm for specializing datatype indices, as described in
--     \"Unifiers as Equivalences: Proof-Relevant Unification of Dependently
--     Typed Data\" by Jesper Cockx, Dominique Devriese, and Frank Piessens
--     (ICFP 2016).
--
--   This is the unification algorithm used for checking the left-hand side
--   of clauses (see @Agda.TypeChecking.Rules.LHS@), coverage checking (see
--   @Agda.TypeChecking.Coverage@) and indirectly also for interactive case
--   splitting (see @Agda.Interaction.MakeCase@).
--
--   A unification problem (of type @UnifyState@) consists of:
--
--   1. A telescope @varTel@ of free variables, some or all of which are
--      flexible (as indicated by @flexVars@).
--
--   2. A telescope @eqTel@ containing the types of the equations.
--
--   3. Left- and right-hand sides for each equation:
--      @varTel ⊢ eqLHS : eqTel@ and @varTel ⊢ eqRHS : eqTel@.
--
--   The unification algorithm can end in three different ways:
--   (type @UnificationResult@):
--
--   - A *positive success* @Unifies (tel, sigma, ps)@ with @tel ⊢ sigma : varTel@,
--     @tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel@,
--     and @tel ⊢ ps : eqTel@. In this case, @sigma;ps@ is an *equivalence*
--     between the telescopes @tel@ and @varTel(eqLHS ≡ eqRHS)@.
--
--   - A *negative success* @NoUnify err@ means that a conflicting equation
--     was found (e.g an equation between two distinct constructors or a cycle).
--
--   - A *failure* @DontKnow err@ means that the unifier got stuck.
--
--   The unification algorithm itself consists of two parts:
--
--   1. A *unification strategy* takes a unification problem and produces a
--      list of suggested unification rules (of type @UnifyStep@). Strategies
--      can be constructed by composing simpler strategies (see for example the
--      definition of @completeStrategyAt@).
--
--   2. The *unification engine* @unifyStep@ takes a unification rule and tries
--      to apply it to the given state, writing the result to the UnifyOutput
--      on a success.
--
--   The unification steps (of type @UnifyStep@) are the following:
--
--   - *Deletion* removes a reflexive equation @u =?= v : a@ if the left- and
--     right-hand side @u@ and @v@ are (definitionally) equal. This rule results
--     in a failure if --without-K is enabled (see \"Pattern Matching Without K\"
--     by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014).
--
--   - *Solution* solves an equation if one side is (eta-equivalent to) a
--     flexible variable. In case both sides are flexible variables, the
--     unification strategy makes a choice according to the @chooseFlex@
--     function in @Agda.TypeChecking.Rules.LHS.Problem@.
--
--   - *Injectivity* decomposes an equation of the form
--     @c us =?= c vs : D pars is@ where @c : Δc → D pars js@ is a constructor
--     of the inductive datatype @D@ into a sequence of equations
--     @us =?= vs : delta@. In case @D@ is an indexed datatype,
--     *higher-dimensional unification* is applied (see below).
--
--   - *Conflict* detects absurd equations of the form
--     @c₁ us =?= c₂ vs : D pars is@ where @c₁@ and @c₂@ are two distinct
--     constructors of the datatype @D@.
--
--   - *Cycle* detects absurd equations of the form @x =?= v : D pars is@ where
--     @x@ is a variable of the datatype @D@ that occurs strongly rigid in @v@.
--
--   - *EtaExpandVar* eta-expands a single flexible variable @x : R@ where @R@
--     is a (eta-expandable) record type, replacing it by one variable for each
--     field of @R@.
--
--   - *EtaExpandEquation* eta-expands an equation @u =?= v : R@ where @R@ is a
--     (eta-expandable) record type, replacing it by one equation for each field
--     of @R@. The left- and right-hand sides of these equations are the
--     projections of @u@ and @v@.
--
--   - *LitConflict* detects absurd equations of the form @l₁ =?= l₂ : A@ where
--     @l₁@ and @l₂@ are distinct literal terms.
--
--   - *StripSizeSuc* simplifies an equation of the form
--     @sizeSuc x =?= sizeSuc y : Size@ to @x =?= y : Size@.
--
--   - *SkipIrrelevantEquation@ removes an equation between irrelevant terms.
--
--   - *TypeConInjectivity* decomposes an equation of the form
--     @D us =?= D vs : Set i@ where @D@ is a datatype. This rule is only used
--     if --injective-type-constructors is enabled.
--
--   Higher-dimensional unification (new, does not yet appear in any paper):
--   If an equation of the form @c us =?= c vs : D pars is@ is encountered where
--   @c : Δc → D pars js@ is a constructor of an indexed datatype
--   @D pars : Φ → Set ℓ@, it is in general unsound to just simplify this
--   equation to @us =?= vs : Δc@. For this reason, the injectivity rule in the
--   paper restricts the indices @is@ to be distinct variables that are bound in
--   the telescope @eqTel@. But we can be more general by introducing new
--   variables @ks@ to the telescope @eqTel@ and equating these to @is@:
--   @
--       Δ₁(x : D pars is)Δ₂
--        ≃
--       Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂
--   @
--   Since @ks@ are distinct variables, it's now possible to apply injectivity
--   to the equation @x@, resulting in the following new equation telescope:
--   @
--     Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂
--   @
--   Now we can solve the equations @ps@ by recursively calling the unification
--   algorithm with flexible variables @Δ₁(ys : Δc)@. This is called
--   *higher-dimensional unification* since we are unifying equality proofs
--   rather than terms. If the higher-dimensional unification succeeds, the
--   resulting telescope serves as the new equation telescope for the original
--   unification problem.

module Agda.TypeChecking.Rules.LHS.Unify
  ( UnificationResult
  , UnificationResult'(..)
  , unifyIndices ) where

import Prelude hiding (null)

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

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

import Data.Foldable (Foldable)
import Data.Traversable (Traversable,traverse)

import Agda.Interaction.Options (optInjectiveTypeConstructors)

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)
import Agda.TypeChecking.Conversion -- equalTerm
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.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.Impossible

-- | Result of 'unifyIndices'.
type UnificationResult = UnificationResult'
  ( Telescope                  -- @tel@
  , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
  , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
  )

data UnificationResult' a
  = Unifies  a                    -- ^ Unification succeeded.
  | NoUnify  NegativeUnification  -- ^ Terms are not unifiable.
  | DontKnow [UnificationFailure] -- ^ Some other error happened, unification got stuck.
  deriving (Int -> UnificationResult' a -> ShowS
[UnificationResult' a] -> ShowS
UnificationResult' a -> String
(Int -> UnificationResult' a -> ShowS)
-> (UnificationResult' a -> String)
-> ([UnificationResult' a] -> ShowS)
-> Show (UnificationResult' a)
forall a. Show a => Int -> UnificationResult' a -> ShowS
forall a. Show a => [UnificationResult' a] -> ShowS
forall a. Show a => UnificationResult' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnificationResult' a] -> ShowS
$cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
show :: UnificationResult' a -> String
$cshow :: forall a. Show a => UnificationResult' a -> String
showsPrec :: Int -> UnificationResult' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> UnificationResult' a -> ShowS
Show, a -> UnificationResult' b -> UnificationResult' a
(a -> b) -> UnificationResult' a -> UnificationResult' b
(forall a b.
 (a -> b) -> UnificationResult' a -> UnificationResult' b)
-> (forall a b. a -> UnificationResult' b -> UnificationResult' a)
-> Functor UnificationResult'
forall a b. a -> UnificationResult' b -> UnificationResult' a
forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> UnificationResult' b -> UnificationResult' a
$c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
fmap :: (a -> b) -> UnificationResult' a -> UnificationResult' b
$cfmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
Functor, UnificationResult' a -> Bool
(a -> m) -> UnificationResult' a -> m
(a -> b -> b) -> b -> UnificationResult' a -> b
(forall m. Monoid m => UnificationResult' m -> m)
-> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
-> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
-> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
-> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
-> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
-> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
-> (forall a. UnificationResult' a -> [a])
-> (forall a. UnificationResult' a -> Bool)
-> (forall a. UnificationResult' a -> Int)
-> (forall a. Eq a => a -> UnificationResult' a -> Bool)
-> (forall a. Ord a => UnificationResult' a -> a)
-> (forall a. Ord a => UnificationResult' a -> a)
-> (forall a. Num a => UnificationResult' a -> a)
-> (forall a. Num a => UnificationResult' a -> a)
-> Foldable UnificationResult'
forall a. Eq a => a -> UnificationResult' a -> Bool
forall a. Num a => UnificationResult' a -> a
forall a. Ord a => UnificationResult' a -> a
forall m. Monoid m => UnificationResult' m -> m
forall a. UnificationResult' a -> Bool
forall a. UnificationResult' a -> Int
forall a. UnificationResult' a -> [a]
forall a. (a -> a -> a) -> UnificationResult' a -> a
forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: UnificationResult' a -> a
$cproduct :: forall a. Num a => UnificationResult' a -> a
sum :: UnificationResult' a -> a
$csum :: forall a. Num a => UnificationResult' a -> a
minimum :: UnificationResult' a -> a
$cminimum :: forall a. Ord a => UnificationResult' a -> a
maximum :: UnificationResult' a -> a
$cmaximum :: forall a. Ord a => UnificationResult' a -> a
elem :: a -> UnificationResult' a -> Bool
$celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
length :: UnificationResult' a -> Int
$clength :: forall a. UnificationResult' a -> Int
null :: UnificationResult' a -> Bool
$cnull :: forall a. UnificationResult' a -> Bool
toList :: UnificationResult' a -> [a]
$ctoList :: forall a. UnificationResult' a -> [a]
foldl1 :: (a -> a -> a) -> UnificationResult' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldr1 :: (a -> a -> a) -> UnificationResult' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldl' :: (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl :: (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldr' :: (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr :: (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldMap' :: (a -> m) -> UnificationResult' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap :: (a -> m) -> UnificationResult' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
fold :: UnificationResult' m -> m
$cfold :: forall m. Monoid m => UnificationResult' m -> m
Foldable, Functor UnificationResult'
Foldable UnificationResult'
Functor UnificationResult'
-> Foldable UnificationResult'
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a))
-> Traversable UnificationResult'
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
sequence :: UnificationResult' (m a) -> m (UnificationResult' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
mapM :: (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
sequenceA :: UnificationResult' (f a) -> f (UnificationResult' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
traverse :: (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$cp2Traversable :: Foldable UnificationResult'
$cp1Traversable :: Functor UnificationResult'
Traversable)

-- | Unify indices.
--
--   In @unifyIndices gamma flex a us vs@,
--
--   * @us@ and @vs@ are the argument lists to unify, eliminating type @a@.
--
--   * @gamma@ is the telescope of free variables in @us@ and @vs@.
--
--   * @flex@ is the set of flexible (instantiable) variabes in @us@ and @vs@.
--
--   The result is the most general unifier of @us@ and @vs@.
unifyIndices
  :: MonadTCM tcm
  => Telescope     -- ^ @gamma@
  -> FlexibleVars  -- ^ @flex@
  -> Type          -- ^ @a@
  -> Args          -- ^ @us@
  -> Args          -- ^ @vs@
  -> tcm UnificationResult
unifyIndices :: Telescope
-> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult
unifyIndices Telescope
tel FlexibleVars
flex Type
a [] [] = UnificationResult -> tcm UnificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult -> tcm UnificationResult)
-> UnificationResult -> tcm UnificationResult
forall a b. (a -> b) -> a -> b
$ (Telescope, Substitution' DeBruijnPattern,
 [NamedArg DeBruijnPattern])
-> UnificationResult
forall a. a -> UnificationResult' a
Unifies (Telescope
tel, Substitution' DeBruijnPattern
forall a. Substitution' a
idS, [])
unifyIndices Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs = TCM UnificationResult -> tcm UnificationResult
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM UnificationResult -> tcm UnificationResult)
-> TCM UnificationResult -> tcm UnificationResult
forall a b. (a -> b) -> a -> b
$ Account Phase -> TCM UnificationResult -> TCM UnificationResult
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.CheckLHS, Phase
Bench.UnifyIndices] (TCM UnificationResult -> TCM UnificationResult)
-> TCM UnificationResult -> TCM UnificationResult
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"unifyIndices"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Int] -> String
forall a. Show a => a -> String
show ([Int] -> String) -> [Int] -> String
forall a b. (a -> b) -> a -> b
$ (FlexibleVar Int -> Int) -> FlexibleVars -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVars
flex
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
us
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
          ]
    UnifyState
initialState    <- Telescope -> FlexibleVars -> Type -> Args -> Args -> TCM UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"initial unifyState:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
initialState
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
70 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"initial unifyState:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (UnifyState -> String
forall a. Show a => a -> String
show UnifyState
initialState)
    (UnificationResult' UnifyState
result,UnifyOutput
output) <- UnifyM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall a. UnifyM a -> TCM (a, UnifyOutput)
runUnifyM (UnifyM (UnificationResult' UnifyState)
 -> TCM (UnificationResult' UnifyState, UnifyOutput))
-> UnifyM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyState
-> UnifyStrategy -> UnifyM (UnificationResult' UnifyState)
unify UnifyState
initialState UnifyStrategy
rightToLeftStrategy
    let ps :: [NamedArg DeBruijnPattern]
ps = Substitution' DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (UnifyOutput -> Substitution' DeBruijnPattern
unifyProof UnifyOutput
output) ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs (UnifyState -> Telescope
eqTel UnifyState
initialState)
    UnificationResult -> TCM UnificationResult
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult -> TCM UnificationResult)
-> UnificationResult -> TCM UnificationResult
forall a b. (a -> b) -> a -> b
$ (UnifyState
 -> (Telescope, Substitution' DeBruijnPattern,
     [NamedArg DeBruijnPattern]))
-> UnificationResult' UnifyState -> UnificationResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\UnifyState
s -> (UnifyState -> Telescope
varTel UnifyState
s , UnifyOutput -> Substitution' DeBruijnPattern
unifySubst UnifyOutput
output , [NamedArg DeBruijnPattern]
ps)) UnificationResult' UnifyState
result

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

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

instance Reduce Equality where
  reduce' :: Equality -> ReduceM Equality
reduce' (Equal Dom Type
a Term
u Term
v) = Dom Type -> Term -> Term -> Equality
Equal (Dom Type -> Term -> Term -> Equality)
-> ReduceM (Dom Type) -> ReduceM (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> ReduceM (Dom Type)
forall t. Reduce t => t -> ReduceM t
reduce' Dom Type
a ReduceM (Term -> Term -> Equality)
-> ReduceM Term -> ReduceM (Term -> Equality)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
u ReduceM (Term -> Equality) -> ReduceM Term -> ReduceM Equality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
v

eqConstructorForm :: Equality -> TCM Equality
eqConstructorForm :: Equality -> TCM Equality
eqConstructorForm (Equal Dom Type
a Term
u Term
v) = Dom Type -> Term -> Term -> Equality
Equal Dom Type
a (Term -> Term -> Equality)
-> TCMT IO Term -> TCMT IO (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m Term
constructorForm Term
u TCMT IO (Term -> Equality) -> TCMT IO Term -> TCM Equality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m Term
constructorForm Term
v

eqUnLevel :: Equality -> TCM Equality
eqUnLevel :: Equality -> TCM Equality
eqUnLevel (Equal Dom Type
a Term
u Term
v) = Dom Type -> Term -> Term -> Equality
Equal Dom Type
a (Term -> Term -> Equality)
-> TCMT IO Term -> TCMT IO (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
u TCMT IO (Term -> Equality) -> TCMT IO Term -> TCM Equality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> TCMT IO 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 (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 -> Args
eqLHS    :: [Arg Term]    -- ^ Ends up in dot patterns (should not be reduced eagerly).
  , UnifyState -> Args
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
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 :: (Telescope -> f Telescope) -> UnifyState -> f 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 :: (Telescope -> f Telescope) -> UnifyState -> f 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 :: 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 :: * -> *). Monad m => [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
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
addContext Telescope
gamma (Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
addContext Telescope
gamma ([m Doc] -> m Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> Arg Term -> m Doc) -> Args -> Args -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
forall (m :: * -> *) a a.
(MonadReduce m, MonadAddContext m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
a -> a -> m Doc
prettyEquality (UnifyState -> Args
eqLHS UnifyState
state) (UnifyState -> Args
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
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
prettyTCM a
y

initUnifyState :: Telescope -> FlexibleVars -> Type -> Args -> Args -> TCM UnifyState
initUnifyState :: Telescope -> FlexibleVars -> Type -> Args -> Args -> TCM UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a Args
lhs Args
rhs = do
  (Telescope
tel, Type
a, Args
lhs, Args
rhs) <- (Telescope, Type, Args, Args)
-> TCMT IO (Telescope, Type, Args, Args)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Telescope
tel, Type
a, Args
lhs, Args
rhs)
  let n :: Int
n = Args -> Int
forall a. Sized a => a -> Int
size Args
lhs
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Args -> Int
forall a. Sized a => a -> Int
size Args
rhs) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  TelV Telescope
eqTel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
  Bool -> TCMT IO () -> TCMT IO ()
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) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  UnifyState -> TCM UnifyState
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyState -> TCM UnifyState) -> UnifyState -> TCM UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope
-> FlexibleVars -> Telescope -> Args -> Args -> UnifyState
UState Telescope
tel FlexibleVars
flex Telescope
eqTel Args
lhs Args
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 Type
getVarType Int
i UnifyState
s = Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i

getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised Int
i UnifyState
s = (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (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 -> Args
eqLHS = Args
lhs, eqRHS :: UnifyState -> Args
eqRHS = Args
rhs } =
    Dom Type -> Term -> Term -> Equality
Equal (Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom Type]
forall a. Subst Term 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 -> Args -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
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 -> Args -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
rhs Int
k)

-- | 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 -> Args
eqLHS = Args
lhs, eqRHS :: UnifyState -> Args
eqRHS = Args
rhs } =
    Dom Type -> Term -> Term -> Equality
Equal ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (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 -> Args -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
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 -> Args -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
rhs Int
k)

--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
-> DeBruijnPattern
-> UnifyState
-> Maybe (UnifyState, Substitution' DeBruijnPattern)
solveVar Int
k DeBruijnPattern
u UnifyState
s = case Telescope
-> Int
-> DeBruijnPattern
-> Maybe (Telescope, Substitution' DeBruijnPattern, Permutation)
instantiateTelescope (UnifyState -> Telescope
varTel UnifyState
s) Int
k DeBruijnPattern
u of
  Maybe (Telescope, Substitution' DeBruijnPattern, Permutation)
Nothing -> Maybe (UnifyState, Substitution' DeBruijnPattern)
forall a. Maybe a
Nothing
  Just (Telescope
tel' , Substitution' DeBruijnPattern
sigma , Permutation
rho) -> (UnifyState, Substitution' DeBruijnPattern)
-> Maybe (UnifyState, Substitution' DeBruijnPattern)
forall a. a -> Maybe a
Just ((UnifyState, Substitution' DeBruijnPattern)
 -> Maybe (UnifyState, Substitution' DeBruijnPattern))
-> (UnifyState, Substitution' DeBruijnPattern)
-> Maybe (UnifyState, Substitution' DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ (,Substitution' DeBruijnPattern
sigma) (UnifyState -> (UnifyState, Substitution' DeBruijnPattern))
-> UnifyState -> (UnifyState, Substitution' DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ UState :: Telescope
-> FlexibleVars -> Telescope -> Args -> Args -> UnifyState
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    = Substitution' DeBruijnPattern -> Telescope -> Telescope
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
sigma (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      , eqLHS :: Args
eqLHS    = Substitution' DeBruijnPattern -> Args -> Args
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
sigma (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
      , eqRHS :: Args
eqRHS    = Substitution' DeBruijnPattern -> Args -> Args
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
sigma (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
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 -> Bool) -> [Int] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (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 Type
a Abs Telescope
tel' -> Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom 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 t a. Subst t a => Abs a -> a
absBody Abs Telescope
tel') Term
u

dropAt :: Int -> [a] -> [a]
dropAt :: 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, Substitution' DeBruijnPattern)
solveEq Int
k Term
u UnifyState
s = (,Substitution' DeBruijnPattern
sigma) (UnifyState -> (UnifyState, Substitution' DeBruijnPattern))
-> UnifyState -> (UnifyState, Substitution' DeBruijnPattern)
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 :: Args
eqLHS    = Int -> Args -> Args
forall a. Int -> [a] -> [a]
dropAt Int
k (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
    , eqRHS :: Args
eqRHS    = Int -> Args -> Args
forall a. Int -> [a] -> [a]
dropAt Int
k (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
    }
  where
    u' :: Term
u'    = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
k Term
u
    n :: Int
n     = UnifyState -> Int
eqCount UnifyState
s
    sigma :: Substitution' DeBruijnPattern
sigma = Int
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
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) (Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern)
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
u') Substitution' DeBruijnPattern
forall a. Substitution' a
idS

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

data UnifyStep
  = Deletion
    { UnifyStep -> Int
deleteAt           :: Int
    , UnifyStep -> Type
deleteType         :: Type
    , UnifyStep -> Term
deleteLeft         :: Term
    , UnifyStep -> Term
deleteRight        :: Term
    }
  | Solution
    { UnifyStep -> Int
solutionAt         :: Int
    , UnifyStep -> Dom Type
solutionType       :: Dom Type
    , UnifyStep -> FlexibleVar Int
solutionVar        :: FlexibleVar Int
    , UnifyStep -> Term
solutionTerm       :: Term
    }
  | Injectivity
    { UnifyStep -> Int
injectAt           :: Int
    , UnifyStep -> Type
injectType         :: Type
    , UnifyStep -> QName
injectDatatype     :: QName
    , UnifyStep -> Args
injectParameters   :: Args
    , UnifyStep -> Args
injectIndices      :: Args
    , UnifyStep -> ConHead
injectConstructor  :: ConHead
    }
  | Conflict
    { UnifyStep -> Int
conflictAt         :: Int
    , UnifyStep -> Type
conflictType       :: Type
    , UnifyStep -> QName
conflictDatatype   :: QName
    , UnifyStep -> Args
conflictParameters :: Args
    , UnifyStep -> Term
conflictLeft       :: Term
    , UnifyStep -> Term
conflictRight      :: Term
    }
  | Cycle
    { UnifyStep -> Int
cycleAt            :: Int
    , UnifyStep -> Type
cycleType          :: Type
    , UnifyStep -> QName
cycleDatatype      :: QName
    , UnifyStep -> Args
cycleParameters    :: Args
    , UnifyStep -> Int
cycleVar           :: Int
    , UnifyStep -> Term
cycleOccursIn      :: Term
    }
  | EtaExpandVar
    { UnifyStep -> FlexibleVar Int
expandVar           :: FlexibleVar Int
    , UnifyStep -> QName
expandVarRecordType :: QName
    , UnifyStep -> Args
expandVarParameters :: Args
    }
  | EtaExpandEquation
    { UnifyStep -> Int
expandAt           :: Int
    , UnifyStep -> QName
expandRecordType   :: QName
    , UnifyStep -> Args
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 -> Args
typeConArgsLeft    :: Args
    , UnifyStep -> Args
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
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 :: 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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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
prettyTCM Term
v
      ])
    Solution Int
k Dom Type
a FlexibleVar Int
i Term
u -> 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 :: * -> *). Monad m => [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 :: * -> *). Monad m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      , m Doc
"type:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
      , m Doc
"variable:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Monad 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
prettyTCM Term
u
      ])
    Injectivity Int
k Type
a QName
d Args
pars Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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
prettyTCM ConHead
c
      ])
    Conflict Int
k Type
a QName
d Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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
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
prettyTCM Term
v
      ])
    Cycle Int
k Type
a QName
d Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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 :: * -> *). Monad 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
prettyTCM Term
u
      ])
    EtaExpandVar FlexibleVar Int
fi QName
r Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
prettyTCM QName
r
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars
      ])
    EtaExpandEquation Int
k QName
r Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
prettyTCM QName
r
      , m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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
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 :: * -> *). Monad m => [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 :: * -> *). Monad m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
      ])
    TypeConInjectivity Int
k QName
d Args
us Args
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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
      ])

type UnifyStrategy = UnifyState -> ListT TCM UnifyStep

--UNUSED Liang-Ting Chen 2019-07-16
--leftToRightStrategy :: UnifyStrategy
--leftToRightStrategy s =
--    msum (for [0..n-1] $ \k -> completeStrategyAt k s)
--  where n = size $ eqTel s

rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy UnifyState
s =
    [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Int] -> (Int -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ((Int -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep])
-> (Int -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
forall a b. (a -> b) -> a -> b
$ \Int
k -> Int -> UnifyStrategy
completeStrategyAt Int
k UnifyState
s)
  where n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s

completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt Int
k UnifyState
s = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([ListT TCM UnifyStep] -> ListT TCM UnifyStep)
-> [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ ((Int -> UnifyStrategy) -> ListT TCM UnifyStep)
-> [Int -> UnifyStrategy] -> [ListT TCM UnifyStep]
forall a b. (a -> b) -> [a] -> [b]
map (\Int -> UnifyStrategy
strat -> Int -> UnifyStrategy
strat Int
k UnifyState
s) ([Int -> UnifyStrategy] -> [ListT TCM UnifyStep])
-> [Int -> UnifyStrategy] -> [ListT TCM UnifyStep]
forall a b. (a -> b) -> a -> b
$
    [ Int -> UnifyStrategy
skipIrrelevantStrategy
    , Int -> UnifyStrategy
basicUnifyStrategy
    , Int -> UnifyStrategy
literalStrategy
    , Int -> UnifyStrategy
dataStrategy
    , Int -> UnifyStrategy
etaExpandVarStrategy
    , Int -> UnifyStrategy
etaExpandEquationStrategy
    , Int -> UnifyStrategy
injectiveTypeConStrategy
    , Int -> UnifyStrategy
injectivePragmaStrategy
    , Int -> UnifyStrategy
simplifySizesStrategy
    , Int -> UnifyStrategy
checkEqualityStrategy
    ]

-- | @isHom n x@ returns x lowered by n if the variables 0..n-1 don't occur in x.
--
-- This is naturally sensitive to normalization.
isHom :: (Free a, Subst Term a) => Int -> a -> Maybe a
isHom :: Int -> a -> Maybe a
isHom Int
n a
x = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar All -> IgnoreSorts -> a -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> All
All (Bool -> All) -> (Int -> Bool) -> SingleVar All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n)) IgnoreSorts
IgnoreNot a
x
  a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Int -> a -> a
forall t a. Subst t a => Int -> a -> a
raise (-Int
n) a
x

findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex =
  let flex' :: [Int]
flex'      = (FlexibleVar Int -> Int) -> FlexibleVars -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVars
flex
      flexible :: Int -> Bool
flexible Int
i = Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
flex'
  in (FlexibleVar Int -> Bool)
-> FlexibleVars -> Maybe (FlexibleVar Int)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool)
-> (FlexibleVar Int -> Int) -> FlexibleVar Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar) FlexibleVars
flex

basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy Int
k UnifyState
s = do
  Equal dom :: Dom Type
dom@Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqUnLevel (Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s)
    -- Andreas, 2019-02-23: reduce equality for the sake of isHom?
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Maybe Type
forall a. (Free a, Subst Term a) => Int -> a -> Maybe a
isHom Int
n Type
a
  (Maybe Int
mi, Maybe Int
mj) <- TCM (Maybe Int, Maybe Int) -> ListT TCM (Maybe Int, Maybe Int)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe Int, Maybe Int) -> ListT TCM (Maybe Int, Maybe Int))
-> TCM (Maybe Int, Maybe Int) -> ListT TCM (Maybe Int, Maybe Int)
forall a b. (a -> b) -> a -> b
$ Telescope
-> TCM (Maybe Int, Maybe Int) -> TCM (Maybe Int, Maybe Int)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (TCM (Maybe Int, Maybe Int) -> TCM (Maybe Int, Maybe Int))
-> TCM (Maybe Int, Maybe Int) -> TCM (Maybe Int, Maybe Int)
forall a b. (a -> b) -> a -> b
$ (,) (Maybe Int -> Maybe Int -> (Maybe Int, Maybe Int))
-> TCMT IO (Maybe Int)
-> TCMT IO (Maybe Int -> (Maybe Int, Maybe Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> TCMT IO (Maybe Int)
isEtaVar Term
u Type
ha TCMT IO (Maybe Int -> (Maybe Int, Maybe Int))
-> TCMT IO (Maybe Int) -> TCM (Maybe Int, Maybe Int)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Type -> TCMT IO (Maybe Int)
isEtaVar Term
v Type
ha
  TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"isEtaVar results: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text ([Maybe Int] -> String
forall a. Show a => a -> String
show [Maybe Int
mi,Maybe Int
mj])
  case (Maybe Int
mi, Maybe Int
mj) of
    (Just Int
i, Just Int
j)
     | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- Taken care of by checkEqualityStrategy
    (Just Int
i, Just Int
j)
     | Just FlexibleVar Int
fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex
     , Just FlexibleVar Int
fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
j FlexibleVars
flex -> do
       let choice :: FlexChoice
choice = FlexibleVar Int -> FlexibleVar Int -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVar Int
fi FlexibleVar Int
fj
           firstTryLeft :: ListT TCM UnifyStep
firstTryLeft  = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v)
                                , UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u)]
           firstTryRight :: ListT TCM UnifyStep
firstTryRight = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u)
                                , UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v)]
       TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"fi = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fi)
       TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"fj = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fj)
       TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"chooseFlex: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (FlexChoice -> String
forall a. Show a => a -> String
show FlexChoice
choice)
       case FlexChoice
choice of
         FlexChoice
ChooseLeft   -> ListT TCM UnifyStep
firstTryLeft
         FlexChoice
ChooseRight  -> ListT TCM UnifyStep
firstTryRight
         FlexChoice
ExpandBoth   -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- This should be taken care of by etaExpandEquationStrategy
         FlexChoice
ChooseEither -> ListT TCM UnifyStep
firstTryRight
    (Just Int
i, Maybe Int
_)
     | Just FlexibleVar Int
fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v
    (Maybe Int
_, Just Int
j)
     | Just FlexibleVar Int
fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
j FlexibleVars
flex -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Dom Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u
    (Maybe Int, Maybe Int)
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    flex :: FlexibleVars
flex = UnifyState -> FlexibleVars
flexVars UnifyState
s
    n :: Int
n = UnifyState -> Int
eqCount UnifyState
s

dataStrategy :: Int -> UnifyStrategy
dataStrategy :: Int -> UnifyStrategy
dataStrategy Int
k UnifyState
s = do
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqConstructorForm (Equality -> TCM Equality) -> TCM Equality -> TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Equality -> TCM Equality
eqUnLevel (Equality -> TCM Equality) -> TCM Equality -> TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Equality -> TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s)
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
es | Type{} <- Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a -> do
      Int
npars <- ListT TCM (Maybe Int) -> ListT TCM Int
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe Int) -> ListT TCM Int)
-> ListT TCM (Maybe Int) -> ListT TCM Int
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe Int) -> ListT TCM (Maybe Int)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Maybe Int) -> ListT TCM (Maybe Int))
-> TCMT IO (Maybe Int) -> ListT TCM (Maybe Int)
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO (Maybe Int)
getNumberOfParameters QName
d
      let (Args
pars,Args
ixs) = Int -> Args -> (Args, Args)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
npars (Args -> (Args, Args)) -> Args -> (Args, Args)
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Found equation at datatype " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
         TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" with parameters " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Args -> Args
forall t a. Subst t a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) Args
pars)
      case (Term
u, Term
v) of
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Args -> ConHead -> UnifyStep
Injectivity Int
k Type
a QName
d Args
pars Args
ixs ConHead
c
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Term -> Term -> UnifyStep
Conflict Int
k Type
a QName
d Args
pars Term
u Term
v
        (Var Int
i []  , Term
v         ) -> Int -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a b.
(MonadTCM m, ForceNotFree a, Reduce a, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i Term
v (ListT TCM UnifyStep -> ListT TCM UnifyStep)
-> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d Args
pars Int
i Term
v
        (Term
u         , Var Int
j []  ) -> Int -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a b.
(MonadTCM m, ForceNotFree a, Reduce a, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
j Term
u (ListT TCM UnifyStep -> ListT TCM UnifyStep)
-> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d Args
pars Int
j Term
u
        (Term, Term)
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    ifOccursStronglyRigid :: Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i a
u m b
ret = do
        -- Call forceNotFree to reduce u as far as possible
        -- around any occurrences of i
        (IntMap IsFree
_ , a
u) <- TCM (IntMap IsFree, a) -> m (IntMap IsFree, a)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (IntMap IsFree, a) -> m (IntMap IsFree, a))
-> TCM (IntMap IsFree, a) -> m (IntMap IsFree, a)
forall a b. (a -> b) -> a -> b
$ IntSet -> a -> TCM (IntMap IsFree, a)
forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree (Int -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton Int
i) a
u
        case Int -> a -> Maybe (FlexRig' ())
forall a. Free a => Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn Int
i a
u of
          Just FlexRig' ()
StronglyRigid -> m b
ret
          Maybe (FlexRig' ())
_ -> m b
forall (m :: * -> *) a. MonadPlus m => m a
mzero

checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy Int
k UnifyState
s = do
  let Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
      n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Maybe Type
forall a. (Free a, Subst Term a) => Int -> a -> Maybe a
isHom Int
n Type
a
  UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Term -> Term -> UnifyStep
Deletion Int
k Type
ha Term
u Term
v

literalStrategy :: Int -> UnifyStrategy
literalStrategy :: Int -> UnifyStrategy
literalStrategy Int
k UnifyState
s = do
  let n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqUnLevel (Equality -> TCM Equality) -> Equality -> TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Maybe Type
forall a. (Free a, Subst Term a) => Int -> a -> Maybe a
isHom Int
n Type
a
  case (Term
u , Term
v) of
    (Lit Literal
l1 , Lit Literal
l2)
     | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2  -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Term -> Term -> UnifyStep
Deletion Int
k Type
ha Term
u Term
v
     | Bool
otherwise -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Literal -> Literal -> UnifyStep
LitConflict Int
k Type
ha Literal
l1 Literal
l2
    (Term, Term)
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero

etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy Int
k UnifyState
s = do
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqUnLevel (Equality -> TCM Equality)
-> (Equality -> TCM Equality) -> Equality -> TCM Equality
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Equality -> TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Equality -> TCM Equality) -> Equality -> TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
u Term
v Type
a UnifyState
s ListT TCM UnifyStep -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
v Term
u Type
a UnifyState
s
  where
    -- TODO: use IsEtaVar to check if the term is a variable
    shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
    shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand (Var Int
i Elims
es) Term
v Type
a UnifyState
s = do
      FlexibleVar Int
fi       <- Maybe (FlexibleVar Int) -> ListT TCM (FlexibleVar Int)
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe (FlexibleVar Int) -> ListT TCM (FlexibleVar Int))
-> Maybe (FlexibleVar Int) -> ListT TCM (FlexibleVar Int)
forall a b. (a -> b) -> a -> b
$ Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i (UnifyState -> FlexibleVars
flexVars UnifyState
s)
      TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Found flexible variable " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i)
      -- Issue 2888: Do this if there are only projections or if it's a singleton
      -- record or if it's unified against a record constructor term. Basically
      -- we need to avoid EtaExpandEquation if EtaExpandVar is possible, or the
      -- forcing translation is unhappy.
      Type
b         <- Type -> ListT TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> ListT TCM Type) -> Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> Dom Type -> Type
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Dom Type
getVarTypeUnraised (UnifyState -> Int
varCount UnifyState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) UnifyState
s
      (QName
d, Args
pars) <- ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args)
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args))
-> ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args)
forall a b. (a -> b) -> a -> b
$ TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args)))
-> TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args))
forall a b. (a -> b) -> a -> b
$ Type -> TCM (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
b
      [(ProjOrigin, QName)]
ps        <- Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)]
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)])
-> Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [(ProjOrigin, QName)]
allProjElims Elims
es
      Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> ListT TCM Bool -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [ListT TCM Bool] -> ListT TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
        [ Bool -> ListT TCM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> ListT TCM Bool) -> Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(ProjOrigin, QName)] -> Bool
forall a. Null a => a -> Bool
null [(ProjOrigin, QName)]
ps
        , TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ Term -> TCM Bool
forall (f :: * -> *). HasConstInfo f => Term -> f Bool
isRecCon Term
v  -- is the other term a record constructor?
        , TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Either MetaId Bool
forall a b. b -> Either a b
Right Bool
True Either MetaId Bool -> Either MetaId Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either MetaId Bool -> Bool)
-> TCMT IO (Either MetaId Bool) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Args -> TCMT IO (Either MetaId Bool)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m,
 ReadTCState m) =>
QName -> Args -> m (Either MetaId Bool)
isSingletonRecord QName
d Args
pars
        ]
      TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"with projections " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
ps)
      TCMT IO () -> ListT TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ListT TCM ()) -> TCMT IO () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"at record type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
      UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ FlexibleVar Int -> QName -> Args -> UnifyStep
EtaExpandVar FlexibleVar Int
fi QName
d Args
pars
    shouldEtaExpand Term
_ Term
_ Type
_ UnifyState
_ = ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    isRecCon :: Term -> f Bool
isRecCon (Con ConHead
c ConInfo
_ Elims
_) = Maybe (QName, Defn) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, Defn) -> Bool) -> f (Maybe (QName, Defn)) -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (ConHead -> QName
conName ConHead
c)
    isRecCon Term
_           = Bool -> f Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy Int
k UnifyState
s = do
  -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Equality -> ListT TCM Equality) -> Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s
  (QName
d, Args
pars) <- ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args)
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args))
-> ListT TCM (Maybe (QName, Args)) -> ListT TCM (QName, Args)
forall a b. (a -> b) -> a -> b
$ TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args)))
-> TCM (Maybe (QName, Args)) -> ListT TCM (Maybe (QName, Args))
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM (Maybe (QName, Args)) -> TCM (Maybe (QName, Args))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM (Maybe (QName, Args)) -> TCM (Maybe (QName, Args)))
-> TCM (Maybe (QName, Args)) -> TCM (Maybe (QName, Args))
forall a b. (a -> b) -> a -> b
$ Type -> TCM (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
a
  Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> ListT TCM Bool -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [ListT TCM Bool] -> ListT TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
    [ TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Either MetaId Bool
forall a b. b -> Either a b
Right Bool
True Either MetaId Bool -> Either MetaId Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either MetaId Bool -> Bool)
-> TCMT IO (Either MetaId Bool) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Args -> TCMT IO (Either MetaId Bool)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m,
 ReadTCState m) =>
QName -> Args -> m (Either MetaId Bool)
isSingletonRecord QName
d Args
pars
    , TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ Term -> TCM Bool
shouldProject Term
u
    , TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ Term -> TCM Bool
shouldProject Term
v
    ]
  UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> QName -> Args -> UnifyStep
EtaExpandEquation Int
k QName
d Args
pars
  where
    shouldProject :: Term -> TCM Bool
    shouldProject :: Term -> TCM Bool
shouldProject Term
u = case Term
u of
      Def QName
f Elims
es   -> QName -> TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
f
      Con ConHead
c ConInfo
_ Elims
_  -> Maybe (QName, Defn) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, Defn) -> Bool)
-> TCMT IO (Maybe (QName, Defn)) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (ConHead -> QName
conName ConHead
c)

      Var Int
_ Elims
_    -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Lam ArgInfo
_ Abs Term
_    -> TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit Literal
_      -> TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Pi Dom Type
_ Abs Type
_     -> TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort Sort' Term
_     -> TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level Level
_    -> TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV MetaId
_ Elims
_  -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      DontCare Term
_ -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Dummy String
s Elims
_  -> String -> TCM Bool
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

    tel :: Telescope
tel = UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` [Dom' Term (String, Type)] -> Telescope
telFromList (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)

simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy Int
k UnifyState
s = do
  QName -> Bool
isSizeName <- TCM (QName -> Bool) -> ListT TCM (QName -> Bool)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM (QName -> Bool)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTest
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Equality -> ListT TCM Equality) -> Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
_ -> do
      Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Bool
isSizeName QName
d
      SizeView
su <- TCM SizeView -> ListT TCM SizeView
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM SizeView -> ListT TCM SizeView)
-> TCM SizeView -> ListT TCM SizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
      SizeView
sv <- TCM SizeView -> ListT TCM SizeView
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM SizeView -> ListT TCM SizeView)
-> TCM SizeView -> ListT TCM SizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
v
      case (SizeView
su, SizeView
sv) of
        (SizeSuc Term
u, SizeSuc Term
v) -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeSuc Term
u, SizeView
SizeInf  ) -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeView
SizeInf  , SizeSuc Term
v) -> UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeView, SizeView)
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy Int
k UnifyState
s = do
  Bool
injTyCon <- TCM Bool -> ListT TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ListT TCM Bool) -> TCM Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optInjectiveTypeConstructors (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
injTyCon
  Equality
eq <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqUnLevel (Equality -> TCM Equality)
-> (Equality -> TCM Equality) -> Equality -> TCM Equality
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Equality -> TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Equality -> TCM Equality) -> Equality -> TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  case Equality
eq of
    Equal Dom Type
a u :: Term
u@(Def QName
d Elims
es) v :: Term
v@(Def QName
d' Elims
es') | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' -> do
      -- d must be a data, record or axiom
      Definition
def <- TCM Definition -> ListT TCM Definition
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Definition -> ListT TCM Definition)
-> TCM Definition -> ListT TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
def of
                Datatype{} -> Bool
True
                Record{}   -> Bool
True
                Axiom{}    -> Bool
True
                DataOrRecSig{} -> Bool
True
                AbstractDefn{} -> Bool
False -- True triggers issue #2250
                Function{}   -> Bool
False
                Primitive{}  -> Bool
False
                GeneralizableVar{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                Constructor{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Never a type!
      let us :: Args
us = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'
      UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> QName -> Args -> Args -> UnifyStep
TypeConInjectivity Int
k QName
d Args
us Args
vs
    Equality
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy Int
k UnifyState
s = do
  Equality
eq <- TCM Equality -> ListT TCM Equality
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Equality -> ListT TCM Equality)
-> TCM Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Equality -> TCM Equality
eqUnLevel (Equality -> TCM Equality)
-> (Equality -> TCM Equality) -> Equality -> TCM Equality
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Equality -> TCM Equality
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Equality -> TCM Equality) -> Equality -> TCM Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  case Equality
eq of
    Equal Dom Type
a u :: Term
u@(Def QName
d Elims
es) v :: Term
v@(Def QName
d' Elims
es') | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' -> do
      -- d must have an injective pragma
      Definition
def <- TCM Definition -> ListT TCM Definition
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Definition -> ListT TCM Definition)
-> TCM Definition -> ListT TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ Definition -> Bool
defInjective Definition
def
      let us :: Args
us = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'
      UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> QName -> Args -> Args -> UnifyStep
TypeConInjectivity Int
k QName
d Args
us Args
vs
    Equality
_ -> ListT TCM UnifyStep
forall (m :: * -> *) a. MonadPlus m => m a
mzero

skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy Int
k UnifyState
s = do
  let Equal Dom Type
a Term
_ Term
_ = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s  -- reduce not necessary
  Bool -> ListT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT TCM ()) -> ListT TCM Bool -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Dom Type -> ListT TCM Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, MonadReduce m,
 MonadDebug m) =>
a -> m Bool
isIrrelevantOrPropM Dom Type
a    -- reduction takes place here
  UnifyStep -> ListT TCM UnifyStep
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> UnifyStep
SkipIrrelevantEquation Int
k


----------------------------------------------------
-- Actually doing the unification
----------------------------------------------------

data UnifyLogEntry
  = UnificationStep  UnifyState UnifyStep
--  | UnificationDone  UnifyState -- unused?

type UnifyLog = [UnifyLogEntry]

data UnifyOutput = UnifyOutput
  { UnifyOutput -> Substitution' DeBruijnPattern
unifySubst :: PatternSubstitution
  , UnifyOutput -> Substitution' DeBruijnPattern
unifyProof :: PatternSubstitution
  , UnifyOutput -> UnifyLog
unifyLog   :: UnifyLog
  }

instance Semigroup UnifyOutput where
  UnifyOutput
x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
<> UnifyOutput
y = UnifyOutput :: Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> UnifyLog -> UnifyOutput
UnifyOutput
    { unifySubst :: Substitution' DeBruijnPattern
unifySubst = UnifyOutput -> Substitution' DeBruijnPattern
unifySubst UnifyOutput
y Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> Substitution' DeBruijnPattern
unifySubst UnifyOutput
x
    , unifyProof :: Substitution' DeBruijnPattern
unifyProof = UnifyOutput -> Substitution' DeBruijnPattern
unifyProof UnifyOutput
y Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> Substitution' DeBruijnPattern
unifyProof UnifyOutput
x
    , unifyLog :: UnifyLog
unifyLog   = UnifyOutput -> UnifyLog
unifyLog UnifyOutput
x UnifyLog -> UnifyLog -> UnifyLog
forall a. [a] -> [a] -> [a]
++ UnifyOutput -> UnifyLog
unifyLog UnifyOutput
y
    }

instance Monoid UnifyOutput where
  mempty :: UnifyOutput
mempty  = Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> UnifyLog -> UnifyOutput
UnifyOutput Substitution' DeBruijnPattern
forall a. Substitution' a
IdS Substitution' DeBruijnPattern
forall a. Substitution' a
IdS []
  mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
mappend = UnifyOutput -> UnifyOutput -> UnifyOutput
forall a. Semigroup a => a -> a -> a
(<>)

type UnifyM a = WriterT UnifyOutput TCM a

tellUnifySubst :: PatternSubstitution -> UnifyM ()
tellUnifySubst :: Substitution' DeBruijnPattern -> UnifyM ()
tellUnifySubst Substitution' DeBruijnPattern
sub = UnifyOutput -> UnifyM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> UnifyM ()) -> UnifyOutput -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> UnifyLog -> UnifyOutput
UnifyOutput Substitution' DeBruijnPattern
sub Substitution' DeBruijnPattern
forall a. Substitution' a
IdS []

tellUnifyProof :: PatternSubstitution -> UnifyM ()
tellUnifyProof :: Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
sub = UnifyOutput -> UnifyM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> UnifyM ()) -> UnifyOutput -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> UnifyLog -> UnifyOutput
UnifyOutput Substitution' DeBruijnPattern
forall a. Substitution' a
IdS Substitution' DeBruijnPattern
sub []

writeUnifyLog :: UnifyLogEntry -> UnifyM ()
writeUnifyLog :: UnifyLogEntry -> UnifyM ()
writeUnifyLog UnifyLogEntry
x = UnifyOutput -> UnifyM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> UnifyM ()) -> UnifyOutput -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> UnifyLog -> UnifyOutput
UnifyOutput Substitution' DeBruijnPattern
forall a. Substitution' a
IdS Substitution' DeBruijnPattern
forall a. Substitution' a
IdS [UnifyLogEntry
x]

runUnifyM :: UnifyM a -> TCM (a,UnifyOutput)
runUnifyM :: UnifyM a -> TCM (a, UnifyOutput)
runUnifyM = UnifyM a -> TCM (a, UnifyOutput)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT

unifyStep :: UnifyState -> UnifyStep -> UnifyM (UnificationResult' UnifyState)

unifyStep :: UnifyState -> UnifyStep -> UnifyM (UnificationResult' UnifyState)
unifyStep UnifyState
s Deletion{ deleteAt :: UnifyStep -> Int
deleteAt = Int
k , deleteType :: UnifyStep -> Type
deleteType = Type
a , deleteLeft :: UnifyStep -> Term
deleteLeft = Term
u , deleteRight :: UnifyStep -> Term
deleteRight = Term
v } = do
    -- Check definitional equality of u and v
    Maybe TCErr
isReflexive <- TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr))
-> TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM (Maybe TCErr) -> TCM (Maybe TCErr)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (TCM (Maybe TCErr) -> TCM (Maybe TCErr))
-> TCM (Maybe TCErr) -> TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCM (Maybe TCErr)
forall e (m :: * -> *).
(MonadError e m, Functor m) =>
m () -> m (Maybe e)
tryCatch (TCMT IO () -> TCM (Maybe TCErr))
-> TCMT IO () -> TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v
    Bool
withoutK <- TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
    case Maybe TCErr
isReflexive of
      Just TCErr
err     -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []
      Maybe TCErr
_ | Bool
withoutK -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [Telescope -> Type -> Term -> UnificationFailure
UnifyReflexiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Term
u]
      Maybe TCErr
_            -> do
        let (UnifyState
s', Substitution' DeBruijnPattern
sigma) = Int
-> Term
-> UnifyState
-> (UnifyState, Substitution' DeBruijnPattern)
solveEq Int
k Term
u UnifyState
s
        Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
sigma
        UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM ((Telescope -> TCMT IO Telescope) -> UnifyState -> TCM UnifyState
Lens' Telescope UnifyState
lensEqTel Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce UnifyState
s')

unifyStep UnifyState
s step :: UnifyStep
step@Solution{} = RetryNormalised
-> UnifyState
-> UnifyStep
-> UnifyM (UnificationResult' UnifyState)
solutionStep RetryNormalised
RetryNormalised UnifyState
s UnifyStep
step

unifyStep UnifyState
s (Injectivity Int
k Type
a QName
d Args
pars Args
ixs ConHead
c) = do
  WriterT UnifyOutput TCM Bool
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT UnifyOutput TCM Bool)
-> TCM Bool -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCM Bool
consOfHIT (QName -> TCM Bool) -> QName -> TCM Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) (UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []) (UnifyM (UnificationResult' UnifyState)
 -> UnifyM (UnificationResult' UnifyState))
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
  Bool
withoutK <- TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
  let n :: Int
n = UnifyState -> Int
eqCount UnifyState
s

  -- Split equation telescope into parts before and after current equation
  let ([Dom' Term (String, Type)]
eqListTel1, Dom' Term (String, Type)
_ : [Dom' Term (String, Type)]
eqListTel2) = Int
-> [Dom' Term (String, Type)]
-> ([Dom' Term (String, Type)], [Dom' Term (String, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
k ([Dom' Term (String, Type)]
 -> ([Dom' Term (String, Type)], [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
      (Telescope
eqTel1, Telescope
eqTel2) = ([Dom' Term (String, Type)] -> Telescope
telFromList [Dom' Term (String, Type)]
eqListTel1, [Dom' Term (String, Type)] -> Telescope
telFromList [Dom' Term (String, Type)]
eqListTel2)

  -- Get constructor telescope and target indices
  Definition
cdef  <- TCM Definition -> WriterT UnifyOutput TCM Definition
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (ConHead -> TCM Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c)
  let ctype :: Type
ctype  = Definition -> Type
defType Definition
cdef Type -> Args -> Type
`piApply` Args
pars
      forced :: [IsForced]
forced = Definition -> [IsForced]
defForced Definition
cdef
  Telescope -> UnifyM () -> UnifyM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"Constructor type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype
  TelV Telescope
ctel Type
ctarget <- TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type))
-> TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ctype
  let cixs :: Args
cixs = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
ctarget of
               Def QName
d' Elims
es | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' ->
                 let args :: Args
args = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                 in  Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
pars) Args
args
               Term
_ -> Args
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- Get index telescope of the datatype
  Type
dtype    <- (Type -> Args -> Type
`piApply` Args
pars) (Type -> Type) -> (Definition -> Type) -> Definition -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> Type)
-> WriterT UnifyOutput TCM Definition
-> WriterT UnifyOutput TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Definition -> WriterT UnifyOutput TCM Definition
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d)
  Telescope -> UnifyM () -> UnifyM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"Datatype type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
dtype

  -- This is where the magic of higher-dimensional unification happens
  -- We need to generalize the indices `ixs` to the target indices of the
  -- constructor `cixs`. This is done by calling the unification algorithm
  -- recursively (this doesn't get stuck in a loop because a type should
  -- never be indexed over itself). Note the similarity with the
  -- computeNeighbourhood function in Agda.TypeChecking.Coverage.
  let hduTel :: Telescope
hduTel = Telescope
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
      notforced :: [IsForced]
notforced = Int -> IsForced -> [IsForced]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
hduTel) IsForced
NotForced
  UnificationResult
res <- TCM UnificationResult -> WriterT UnifyOutput TCM UnificationResult
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM UnificationResult
 -> WriterT UnifyOutput TCM UnificationResult)
-> TCM UnificationResult
-> WriterT UnifyOutput TCM UnificationResult
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM UnificationResult -> TCM UnificationResult
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (TCM UnificationResult -> TCM UnificationResult)
-> TCM UnificationResult -> TCM UnificationResult
forall a b. (a -> b) -> a -> b
$ Telescope
-> FlexibleVars -> Type -> Args -> Args -> TCM UnificationResult
forall (tcm :: * -> *).
MonadTCM tcm =>
Telescope
-> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult
unifyIndices
           Telescope
hduTel
           ([IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
notforced Telescope
hduTel)
           (Int -> Type -> Type
forall t a. Subst t a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ctel) Type
dtype)
           (Int -> Args -> Args
forall t a. Subst t a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ctel) Args
ixs)
           Args
cixs
  case UnificationResult
res of
    -- Higher-dimensional unification can never end in a conflict,
    -- because `cong c1 ...` and `cong c2 ...` don't even have the
    -- same type for distinct constructors c1 and c2.
    NoUnify NegativeUnification
_ -> UnifyM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Higher-dimensional unification has failed. If not --without-K,
    -- we can simply ignore the higher-dimensional equations and
    -- simplify the equation as in the non-indexed case.
    DontKnow [UnificationFailure]
_ | Bool -> Bool
not Bool
withoutK -> do
      -- using the same variable names as in the case where hdu succeeds.
      let eqTel1' :: Telescope
eqTel1' = Telescope
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
          rho1 :: Substitution' a
rho1    = Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ctel)
          ceq :: DeBruijnPattern
ceq     = ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: Substitution' DeBruijnPattern
rho3    = DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
ceq Substitution' DeBruijnPattern
forall a. Substitution' a
rho1
          eqTel2' :: Telescope
eqTel2' = Substitution' DeBruijnPattern -> Telescope -> Telescope
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: Substitution' DeBruijnPattern
rho     = Int
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel2) Substitution' DeBruijnPattern
rho3

      Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
rho

      Telescope
eqTel' <- TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope)
-> TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Telescope
eqTel'

      -- Compute new lhs and rhs by matching the old ones against rho
      (Args
lhs', Args
rhs') <- do
        let ps :: [NamedArg DeBruijnPattern]
ps = Substitution' DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs (Telescope -> [NamedArg DeBruijnPattern])
-> Telescope -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (Match Term
lhsMatch, Args
_) <- TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Match Term, Args)
 -> WriterT UnifyOutput TCM (Match Term, Args))
-> TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Match Term, Args) -> TCM (Match Term, Args))
-> ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Args -> ReduceM (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps (Args -> ReduceM (Match Term, Args))
-> Args -> ReduceM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
        (Match Term
rhsMatch, Args
_) <- TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Match Term, Args)
 -> WriterT UnifyOutput TCM (Match Term, Args))
-> TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Match Term, Args) -> TCM (Match Term, Args))
-> ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Args -> ReduceM (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps (Args -> ReduceM (Match Term, Args))
-> Args -> ReduceM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
        case (Match Term
lhsMatch, Match Term
rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> (Args, Args) -> WriterT UnifyOutput TCM (Args, Args)
forall (m :: * -> *) a. Monad m => a -> m a
return
            (Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Empty -> Int -> IntMap (Arg Term) -> Args
forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
             Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Empty -> Int -> IntMap (Arg Term) -> Args
forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> WriterT UnifyOutput TCM (Args, Args)
forall a. HasCallStack => a
__IMPOSSIBLE__

      UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s { eqTel :: Telescope
eqTel = Telescope
eqTel' , eqLHS :: Args
eqLHS = Args
lhs' , eqRHS :: Args
eqRHS = Args
rhs' }


    DontKnow [UnificationFailure]
_ -> let n :: Int
n           = UnifyState -> Int
eqCount UnifyState
s
                      Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
                  in UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [Telescope -> Type -> Term -> Term -> Args -> UnificationFailure
UnifyIndicesNotVars
                       (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) Type
a
                       (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
n Term
u) (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
n Term
v) (Int -> Args -> Args
forall t a. Subst t a => Int -> a -> a
raise (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
k) Args
ixs)]

    Unifies (Telescope
eqTel1', Substitution' DeBruijnPattern
rho0, [NamedArg DeBruijnPattern]
_) -> do
      -- Split ps0 into parts for eqTel1 and ctel
      let (Substitution' DeBruijnPattern
rho1, Substitution' DeBruijnPattern
rho2) = Int
-> Substitution' DeBruijnPattern
-> (Substitution' DeBruijnPattern, Substitution' DeBruijnPattern)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ctel) Substitution' DeBruijnPattern
rho0

      -- Compute new equation telescope context and substitution
      let ceq :: DeBruijnPattern
ceq     = ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho2 ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: Substitution' DeBruijnPattern
rho3    = DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
ceq Substitution' DeBruijnPattern
rho1
          eqTel2' :: Telescope
eqTel2' = Substitution' DeBruijnPattern -> Telescope -> Telescope
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: Substitution' DeBruijnPattern
rho     = Int
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel2) Substitution' DeBruijnPattern
rho3

      Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
rho

      Telescope
eqTel' <- TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope)
-> TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Telescope
eqTel'

      -- Compute new lhs and rhs by matching the old ones against rho
      (Args
lhs', Args
rhs') <- do
        let ps :: [NamedArg DeBruijnPattern]
ps = Substitution' DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs (Telescope -> [NamedArg DeBruijnPattern])
-> Telescope -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (Match Term
lhsMatch, Args
_) <- TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Match Term, Args)
 -> WriterT UnifyOutput TCM (Match Term, Args))
-> TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Match Term, Args) -> TCM (Match Term, Args))
-> ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Args -> ReduceM (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps (Args -> ReduceM (Match Term, Args))
-> Args -> ReduceM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
        (Match Term
rhsMatch, Args
_) <- TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Match Term, Args)
 -> WriterT UnifyOutput TCM (Match Term, Args))
-> TCM (Match Term, Args)
-> WriterT UnifyOutput TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a. ReduceM a -> TCM a
runReduceM (ReduceM (Match Term, Args) -> TCM (Match Term, Args))
-> ReduceM (Match Term, Args) -> TCM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Args -> ReduceM (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps (Args -> ReduceM (Match Term, Args))
-> Args -> ReduceM (Match Term, Args)
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
        case (Match Term
lhsMatch, Match Term
rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> (Args, Args) -> WriterT UnifyOutput TCM (Args, Args)
forall (m :: * -> *) a. Monad m => a -> m a
return
            (Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Empty -> Int -> IntMap (Arg Term) -> Args
forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
             Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Empty -> Int -> IntMap (Arg Term) -> Args
forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> WriterT UnifyOutput TCM (Args, Args)
forall a. HasCallStack => a
__IMPOSSIBLE__

      UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s { eqTel :: Telescope
eqTel = Telescope
eqTel' , eqLHS :: Args
eqLHS = Args
lhs' , eqRHS :: Args
eqRHS = Args
rhs' }

unifyStep UnifyState
s Conflict
  { conflictLeft :: UnifyStep -> Term
conflictLeft  = Term
u
  , conflictRight :: UnifyStep -> Term
conflictRight = Term
v
  } =
  case Term
u of
    Con ConHead
h ConInfo
_ Elims
_ -> do
      WriterT UnifyOutput TCM Bool
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT UnifyOutput TCM Bool)
-> TCM Bool -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCM Bool
consOfHIT (QName -> TCM Bool) -> QName -> TCM Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []) (UnifyM (UnificationResult' UnifyState)
 -> UnifyM (UnificationResult' UnifyState))
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify (NegativeUnification -> UnificationResult' UnifyState)
-> NegativeUnification -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) Term
u Term
v
    Term
_ -> UnifyM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__
unifyStep UnifyState
s Cycle
  { cycleVar :: UnifyStep -> Int
cycleVar        = Int
i
  , cycleOccursIn :: UnifyStep -> Term
cycleOccursIn   = Term
u
  } =
  case Term
u of
    Con ConHead
h ConInfo
_ Elims
_ -> do
      WriterT UnifyOutput TCM Bool
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT UnifyOutput TCM Bool)
-> TCM Bool -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCM Bool
consOfHIT (QName -> TCM Bool) -> QName -> TCM Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []) (UnifyM (UnificationResult' UnifyState)
 -> UnifyM (UnificationResult' UnifyState))
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify (NegativeUnification -> UnificationResult' UnifyState)
-> NegativeUnification -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope -> Int -> Term -> NegativeUnification
UnifyCycle (UnifyState -> Telescope
varTel UnifyState
s) Int
i Term
u
    Term
_ -> UnifyM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unifyStep UnifyState
s EtaExpandVar{ expandVar :: UnifyStep -> FlexibleVar Int
expandVar = FlexibleVar Int
fi, expandVarRecordType :: UnifyStep -> QName
expandVarRecordType = QName
d , expandVarParameters :: UnifyStep -> Args
expandVarParameters = Args
pars } = do
  Telescope
delta   <- TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope)
-> TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ (Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars) (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Telescope
getRecordFieldTypes QName
d
  ConHead
c       <- TCM ConHead -> WriterT UnifyOutput TCM ConHead
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM ConHead -> WriterT UnifyOutput TCM ConHead)
-> TCM ConHead -> WriterT UnifyOutput TCM ConHead
forall a b. (a -> b) -> a -> b
$ QName -> TCM ConHead
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
d
  let nfields :: Int
nfields         = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta
      (Telescope
varTel', Substitution' DeBruijnPattern
rho)  = Telescope
-> Int
-> Telescope
-> ConHead
-> (Telescope, Substitution' DeBruijnPattern)
expandTelescopeVar (UnifyState -> Telescope
varTel UnifyState
s) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) Telescope
delta ConHead
c
      projectFlexible :: FlexibleVars
projectFlexible = [ ArgInfo
-> IsForced
-> FlexibleVarKind
-> Maybe Int
-> Int
-> FlexibleVar Int
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar (FlexibleVar Int -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo FlexibleVar Int
fi) (FlexibleVar Int -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
fi) (Int -> FlexibleVarKind
projFlexKind Int
j) (FlexibleVar Int -> Maybe Int
forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
fi) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j) | Int
j <- [Int
0..Int
nfieldsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
  Substitution' DeBruijnPattern -> UnifyM ()
tellUnifySubst (Substitution' DeBruijnPattern -> UnifyM ())
-> Substitution' DeBruijnPattern -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern
rho
  UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UState :: Telescope
-> FlexibleVars -> Telescope -> Args -> Args -> UnifyState
UState
    { varTel :: Telescope
varTel   = Telescope
varTel'
    , flexVars :: FlexibleVars
flexVars = FlexibleVars
projectFlexible FlexibleVars -> FlexibleVars -> FlexibleVars
forall a. [a] -> [a] -> [a]
++ Int -> FlexibleVars -> FlexibleVars
liftFlexibles Int
nfields (UnifyState -> FlexibleVars
flexVars UnifyState
s)
    , eqTel :: Telescope
eqTel    = Substitution' DeBruijnPattern -> Telescope -> Telescope
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
    , eqLHS :: Args
eqLHS    = Substitution' DeBruijnPattern -> Args -> Args
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
    , eqRHS :: Args
eqRHS    = Substitution' DeBruijnPattern -> Args -> Args
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
    }
  where
    i :: Int
i = FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fi
    m :: Int
m = UnifyState -> Int
varCount UnifyState
s
    n :: Int
n = UnifyState -> Int
eqCount UnifyState
s

    projFlexKind :: Int -> FlexibleVarKind
    projFlexKind :: Int -> FlexibleVarKind
projFlexKind Int
j = case FlexibleVar Int -> FlexibleVarKind
forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
fi of
      RecordFlex [FlexibleVarKind]
ks -> FlexibleVarKind -> [FlexibleVarKind] -> Int -> FlexibleVarKind
forall a. a -> [a] -> Int -> a
indexWithDefault FlexibleVarKind
ImplicitFlex [FlexibleVarKind]
ks Int
j
      FlexibleVarKind
ImplicitFlex  -> FlexibleVarKind
ImplicitFlex
      FlexibleVarKind
DotFlex       -> FlexibleVarKind
DotFlex
      FlexibleVarKind
OtherFlex     -> FlexibleVarKind
OtherFlex

    liftFlexible :: Int -> Int -> Maybe Int
    liftFlexible :: Int -> Int -> Maybe Int
liftFlexible Int
n Int
j = if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then Maybe Int
forall a. Maybe a
Nothing else Int -> Maybe Int
forall a. a -> Maybe a
Just (if Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i then Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) else Int
j)

    liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
    liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
liftFlexibles Int
n FlexibleVars
fs = (FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars -> FlexibleVars
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int))
-> (Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Maybe Int
liftFlexible Int
n) FlexibleVars
fs

unifyStep UnifyState
s EtaExpandEquation{ expandAt :: UnifyStep -> Int
expandAt = Int
k, expandRecordType :: UnifyStep -> QName
expandRecordType = QName
d, expandParameters :: UnifyStep -> Args
expandParameters = Args
pars } = do
  Telescope
delta <- TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope)
-> TCMT IO Telescope -> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ (Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars) (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Telescope
getRecordFieldTypes QName
d
  ConHead
c     <- TCM ConHead -> WriterT UnifyOutput TCM ConHead
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM ConHead -> WriterT UnifyOutput TCM ConHead)
-> TCM ConHead -> WriterT UnifyOutput TCM ConHead
forall a b. (a -> b) -> a -> b
$ QName -> TCM ConHead
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
d
  Args
lhs   <- Args -> WriterT UnifyOutput TCM Args
forall (m :: * -> *). MonadTCM m => Args -> m Args
expandKth (Args -> WriterT UnifyOutput TCM Args)
-> Args -> WriterT UnifyOutput TCM Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
  Args
rhs   <- Args -> WriterT UnifyOutput TCM Args
forall (m :: * -> *). MonadTCM m => Args -> m Args
expandKth (Args -> WriterT UnifyOutput TCM Args)
-> Args -> WriterT UnifyOutput TCM Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
  let (Telescope
tel, Substitution' DeBruijnPattern
sigma) = Telescope
-> Int
-> Telescope
-> ConHead
-> (Telescope, Substitution' DeBruijnPattern)
expandTelescopeVar (UnifyState -> Telescope
eqTel UnifyState
s) Int
k Telescope
delta ConHead
c
  Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
sigma
  UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
   TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ (Telescope -> TCMT IO Telescope) -> UnifyState -> TCM UnifyState
Lens' Telescope UnifyState
lensEqTel Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (UnifyState -> TCM UnifyState) -> UnifyState -> TCM UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel :: Telescope
eqTel    = Telescope
tel
    , eqLHS :: Args
eqLHS    = Args
lhs
    , eqRHS :: Args
eqRHS    = Args
rhs
    }
  where
    expandKth :: Args -> m Args
expandKth Args
us = do
      let (Args
us1,Arg Term
v:Args
us2) = (Args, Args) -> Maybe (Args, Args) -> (Args, Args)
forall a. a -> Maybe a -> a
fromMaybe (Args, Args)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Args, Args) -> (Args, Args))
-> Maybe (Args, Args) -> (Args, Args)
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Maybe (Args, Args)
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k Args
us
      Args
vs <- TCM Args -> m Args
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Args -> m Args) -> TCM Args -> m Args
forall a b. (a -> b) -> a -> b
$ (Telescope, Args) -> Args
forall a b. (a, b) -> b
snd ((Telescope, Args) -> Args)
-> TCMT IO (Telescope, Args) -> TCM Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Args -> Term -> TCMT IO (Telescope, Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m,
 MonadError TCErr m) =>
QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord QName
d Args
pars (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v)
      Args
vs <- TCM Args -> m Args
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Args -> m Args) -> TCM Args -> m Args
forall a b. (a -> b) -> a -> b
$ Args -> TCM Args
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Args
vs
      Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return (Args -> m Args) -> Args -> m Args
forall a b. (a -> b) -> a -> b
$ Args
us1 Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
us2

unifyStep UnifyState
s LitConflict
  { litType :: UnifyStep -> Type
litType          = Type
a
  , litConflictLeft :: UnifyStep -> Literal
litConflictLeft  = Literal
l
  , litConflictRight :: UnifyStep -> Literal
litConflictRight = Literal
l'
  } = UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify (NegativeUnification -> UnificationResult' UnifyState)
-> NegativeUnification -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) (Literal -> Term
Lit Literal
l) (Literal -> Term
Lit Literal
l')

unifyStep UnifyState
s (StripSizeSuc Int
k Term
u Term
v) = do
  Type
sizeTy <- TCM Type -> WriterT UnifyOutput TCM Type
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  Term
sizeSu <- TCMT IO Term -> WriterT UnifyOutput TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> WriterT UnifyOutput TCM Term)
-> TCMT IO Term -> WriterT UnifyOutput TCM Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 (Int -> Term
var Int
0)
  let n :: Int
n          = UnifyState -> Int
eqCount UnifyState
s
      sub :: Substitution' Term
sub        = Int -> Substitution' Term -> Substitution' Term
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) (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
sizeSu (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1
      eqFlatTel :: [Dom Type]
eqFlatTel  = Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      eqFlatTel' :: [Dom Type]
eqFlatTel' = Substitution' Term -> [Dom Type] -> [Dom Type]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Int -> (Dom Type -> Dom Type) -> [Dom Type] -> [Dom Type]
forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k ((Type -> Type) -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Type -> Type) -> Dom Type -> Dom Type)
-> (Type -> Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
forall a b. a -> b -> a
const Type
sizeTy) ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ [Dom Type]
eqFlatTel
      eqTel' :: Telescope
eqTel'     = [String] -> [Dom Type] -> Telescope
unflattenTel (Telescope -> [String]
teleNames (Telescope -> [String]) -> Telescope -> [String]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) [Dom Type]
eqFlatTel'
  -- TODO: tellUnifyProof sub
  -- but sizeSu is not a constructor, so sub is not a PatternSubstitution!
  UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel :: Telescope
eqTel = Telescope
eqTel'
    , eqLHS :: Args
eqLHS = Int -> (Arg Term -> Arg Term) -> Args -> Args
forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (Arg Term -> Arg Term -> Arg Term
forall a b. a -> b -> a
const (Arg Term -> Arg Term -> Arg Term)
-> Arg Term -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
u) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
    , eqRHS :: Args
eqRHS = Int -> (Arg Term -> Arg Term) -> Args -> Args
forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (Arg Term -> Arg Term -> Arg Term
forall a b. a -> b -> a
const (Arg Term -> Arg Term -> Arg Term)
-> Arg Term -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
    }

unifyStep UnifyState
s (SkipIrrelevantEquation Int
k) = do
  let lhs :: Args
lhs = UnifyState -> Args
eqLHS UnifyState
s
      (UnifyState
s', Substitution' DeBruijnPattern
sigma) = Int
-> Term
-> UnifyState
-> (UnifyState, Substitution' DeBruijnPattern)
solveEq Int
k (Term -> Term
DontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Args -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
lhs Int
k) UnifyState
s
  Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
sigma
  UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s'

unifyStep UnifyState
s (TypeConInjectivity Int
k QName
d Args
us Args
vs) = do
  Type
dtype <- Definition -> Type
defType (Definition -> Type)
-> WriterT UnifyOutput TCM Definition
-> WriterT UnifyOutput TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Definition -> WriterT UnifyOutput TCM Definition
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d)
  TelV Telescope
dtel Type
_ <- TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type))
-> TCMT IO (TelV Type) -> WriterT UnifyOutput TCM (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
dtype
  let n :: Int
n   = UnifyState -> Int
eqCount UnifyState
s
      m :: Int
m   = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
dtel
      deq :: Term
deq = QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
dtel
  -- TODO: tellUnifyProof ???
  -- but d is not a constructor...
  UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
   TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ (Telescope -> TCMT IO Telescope) -> UnifyState -> TCM UnifyState
Lens' Telescope UnifyState
lensEqTel Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (UnifyState -> TCM UnifyState) -> UnifyState -> TCM UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel :: Telescope
eqTel = Telescope
dtel Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Int -> Telescope -> Term -> Telescope
applyUnder Int
k (UnifyState -> Telescope
eqTel UnifyState
s) (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
k Term
deq)
    , eqLHS :: Args
eqLHS = Args
us Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Int -> Args -> Args
forall a. Int -> [a] -> [a]
dropAt Int
k (UnifyState -> Args
eqLHS UnifyState
s)
    , eqRHS :: Args
eqRHS = Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Int -> Args -> Args
forall a. Int -> [a] -> [a]
dropAt Int
k (UnifyState -> Args
eqRHS UnifyState
s)
    }

data RetryNormalised = RetryNormalised | DontRetryNormalised
  deriving (RetryNormalised -> RetryNormalised -> Bool
(RetryNormalised -> RetryNormalised -> Bool)
-> (RetryNormalised -> RetryNormalised -> Bool)
-> Eq RetryNormalised
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RetryNormalised -> RetryNormalised -> Bool
$c/= :: RetryNormalised -> RetryNormalised -> Bool
== :: RetryNormalised -> RetryNormalised -> Bool
$c== :: RetryNormalised -> RetryNormalised -> Bool
Eq, Int -> RetryNormalised -> ShowS
[RetryNormalised] -> ShowS
RetryNormalised -> String
(Int -> RetryNormalised -> ShowS)
-> (RetryNormalised -> String)
-> ([RetryNormalised] -> ShowS)
-> Show RetryNormalised
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RetryNormalised] -> ShowS
$cshowList :: [RetryNormalised] -> ShowS
show :: RetryNormalised -> String
$cshow :: RetryNormalised -> String
showsPrec :: Int -> RetryNormalised -> ShowS
$cshowsPrec :: Int -> RetryNormalised -> ShowS
Show)

solutionStep :: RetryNormalised -> UnifyState -> UnifyStep -> UnifyM (UnificationResult' UnifyState)
solutionStep :: RetryNormalised
-> UnifyState
-> UnifyStep
-> UnifyM (UnificationResult' UnifyState)
solutionStep RetryNormalised
retry UnifyState
s
  step :: UnifyStep
step@Solution{ solutionAt :: UnifyStep -> Int
solutionAt   = Int
k
               , solutionType :: UnifyStep -> Dom Type
solutionType = dom :: Dom Type
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a }
               , solutionVar :: UnifyStep -> FlexibleVar Int
solutionVar  = fi :: FlexibleVar Int
fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
flexVar = Int
i }
               , solutionTerm :: UnifyStep -> Term
solutionTerm = Term
u } = do
  let m :: Int
m = UnifyState -> Int
varCount UnifyState
s

  -- Now we have to be careful about forced variables in `u`. If they appear
  -- in pattern positions we need to bind them there rather in their forced positions. We can safely
  -- ignore non-pattern positions and forced pattern positions, because in that case there will be
  -- other equations where the variable can be bound.
  -- NOTE: If we're doing make-case we ignore forced variables. This is safe since we take the
  -- result of unification and build user clauses that will be checked again with forcing turned on.
  Bool
inMakeCase <- Lens' Bool TCEnv -> WriterT UnifyOutput TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eMakeCase
  let forcedVars :: IntMap Modality
forcedVars | Bool
inMakeCase = IntMap Modality
forall a. IntMap a
IntMap.empty
                 | Bool
otherwise  = [(Int, Modality)] -> IntMap Modality
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [ (FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fi, FlexibleVar Int -> Modality
forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) | FlexibleVar Int
fi <- UnifyState -> FlexibleVars
flexVars UnifyState
s,
                                                                                 FlexibleVar Int -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
fi IsForced -> IsForced -> Bool
forall a. Eq a => a -> a -> Bool
== IsForced
Forced ]
  (DeBruijnPattern
p, IntMap Modality
bound) <- IntMap Modality
-> Term
-> WriterT UnifyOutput TCM (DeBruijnPattern, IntMap Modality)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars IntMap Modality
forcedVars Term
u

  -- To maintain the invariant that each variable in varTel is bound exactly once in the pattern
  -- subtitution we need to turn the bound variables in `p` into dot patterns in the rest of the
  -- substitution.
  let dotSub :: Substitution' DeBruijnPattern
dotSub = (Substitution' DeBruijnPattern
 -> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern)
-> Substitution' DeBruijnPattern
-> [Substitution' DeBruijnPattern]
-> Substitution' DeBruijnPattern
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' DeBruijnPattern
forall a. Substitution' a
idS [ Int -> DeBruijnPattern -> Substitution' DeBruijnPattern
forall a. Subst a a => Int -> a -> Substitution' a
inplaceS Int
i (Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])) | Int
i <- IntMap Modality -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
bound ]

  -- We moved the binding site of some forced variables, so we need to update their modalities in
  -- the telescope. The new modality is the combination of the modality of the variable we are
  -- instantiating and the modality of the binding site in the pattern (return by
  -- patternBindingForcedVars).
  let updModality :: Modality -> IntMap Modality -> Telescope -> Telescope
updModality Modality
md IntMap Modality
vars Telescope
tel
        | IntMap Modality -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Modality
vars = Telescope
tel
        | Bool
otherwise        = [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))
-> [Int]
-> [Dom' Term (String, Type)]
-> [Dom' Term (String, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom' Term (String, Type) -> Dom' Term (String, Type)
forall p. LensModality p => Int -> p -> p
upd (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
        where
          upd :: Int -> p -> p
upd Int
i p
a | Just Modality
md' <- Int -> IntMap Modality -> Maybe Modality
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Modality
vars = Modality -> p -> p
forall a. LensModality a => Modality -> a -> a
setModality (Modality
md Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<> Modality
md') p
a
                  | Bool
otherwise                        = p
a
  UnifyState
s <- UnifyState -> WriterT UnifyOutput TCM UnifyState
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s { varTel :: Telescope
varTel = Modality -> IntMap Modality -> Telescope -> Telescope
updModality (FlexibleVar Int -> Modality
forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) IntMap Modality
bound (UnifyState -> Telescope
varTel UnifyState
s) }

  String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify.force" Int
45 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"forcedVars =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Int] -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (IntMap Modality -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
forcedVars)
    , TCM Doc
"u          =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
    , TCM Doc
"p          =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p
    , TCM Doc
"bound      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Int] -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (IntMap Modality -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
bound)
    , TCM Doc
"dotSub     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' DeBruijnPattern -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Substitution' DeBruijnPattern
dotSub ]

  -- Check that the type of the variable is equal to the type of the equation
  -- (not just a subtype), otherwise we cannot instantiate (see Issue 2407).
  let dom' :: Dom Type
dom'@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a' } = Int -> UnifyState -> Dom Type
getVarType (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) UnifyState
s
  Maybe TCErr
equalTypes <- TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr))
-> TCM (Maybe TCErr) -> WriterT UnifyOutput TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM (Maybe TCErr) -> TCM (Maybe TCErr)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (TCM (Maybe TCErr) -> TCM (Maybe TCErr))
-> TCM (Maybe TCErr) -> TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCM (Maybe TCErr)
forall e (m :: * -> *).
(MonadError e m, Functor m) =>
m () -> m (Maybe e)
tryCatch (TCMT IO () -> TCM (Maybe TCErr))
-> TCMT IO () -> TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Equation type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Variable type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a'
    TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a Type
a'

  -- The conditions on the relevances are as follows (see #2640):
  -- - If the type of the equation is relevant, then the solution must be
  --   usable in a relevant position.
  -- - If the type of the equation is (shape-)irrelevant, then the solution
  --   must be usable in a μ-relevant position where μ is the relevance
  --   of the variable being solved.
  --
  -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally
  -- always @Quantity0@, since the indices of the data type are runtime erased.
  -- Thus, we need not change the quantity of the solution.
  let eqrel :: Relevance
eqrel  = Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom
      eqmod :: Modality
eqmod  = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom
      varmod :: Modality
varmod = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom'
      mod :: Modality
mod    = Bool -> (Modality -> Modality) -> Modality -> Modality
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Relevance
NonStrict Relevance -> Relevance -> Bool
`moreRelevant` Relevance
eqrel) (Relevance -> Modality -> Modality
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
eqrel)
             (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Modality
varmod
  String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"Equation modality: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show (Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom)
  String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"Variable modality: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show Modality
varmod
  String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"Solution must be usable in a " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show Modality
mod String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" position."
  -- Andreas, 2018-10-18
  -- Currently, the modality check has problems with meta-variables created in the type signature,
  -- and thus, in quantity 0, that get into terms using the unifier, and there are checked to be
  -- non-erased, i.e., have quantity ω.
  -- Ulf, 2019-12-13. We still do it though.
  Bool
usable <- TCM Bool -> WriterT UnifyOutput TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT UnifyOutput TCM Bool)
-> TCM Bool -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Bool -> TCM Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ Modality -> Term -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Term
u
  String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Modality ok: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
usable
  Bool -> UnifyM () -> UnifyM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
usable (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.lhs.unify" Int
65 (String -> UnifyM ()) -> String -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ String
"Rejected solution: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
u

  -- We need a Flat equality to solve a Flat variable.
  -- This also ought to take care of the need for a usableCohesion check.
  if Bool -> Bool
not (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
eqmod Cohesion -> Cohesion -> Bool
`moreCohesion` Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
varmod) then UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [] else do

  case Maybe TCErr
equalTypes of
    Just TCErr
err -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []
    Maybe TCErr
Nothing | Bool
usable ->
      case Int
-> DeBruijnPattern
-> UnifyState
-> Maybe (UnifyState, Substitution' DeBruijnPattern)
solveVar (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) DeBruijnPattern
p UnifyState
s of
        Maybe (UnifyState, Substitution' DeBruijnPattern)
Nothing | RetryNormalised
retry RetryNormalised -> RetryNormalised -> Bool
forall a. Eq a => a -> a -> Bool
== RetryNormalised
RetryNormalised -> do
          Term
u <- TCMT IO Term -> WriterT UnifyOutput TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> WriterT UnifyOutput TCM Term)
-> TCMT IO Term -> WriterT UnifyOutput TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
u
          UnifyState
s <- TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> TCM UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ (Telescope -> TCMT IO Telescope) -> UnifyState -> TCM UnifyState
Lens' Telescope UnifyState
lensVarTel Telescope -> TCMT IO Telescope
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise UnifyState
s
          RetryNormalised
-> UnifyState
-> UnifyStep
-> UnifyM (UnificationResult' UnifyState)
solutionStep RetryNormalised
DontRetryNormalised UnifyState
s UnifyStep
step{ solutionTerm :: Term
solutionTerm = Term
u }
        Maybe (UnifyState, Substitution' DeBruijnPattern)
Nothing ->
          UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [Telescope -> Type -> Int -> Term -> UnificationFailure
UnifyRecursiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u]
        Just (UnifyState
s', Substitution' DeBruijnPattern
sub) -> do
          let rho :: Substitution' DeBruijnPattern
rho = Substitution' DeBruijnPattern
sub Substitution' DeBruijnPattern
-> Substitution' DeBruijnPattern -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' DeBruijnPattern
dotSub
          Substitution' DeBruijnPattern -> UnifyM ()
tellUnifySubst Substitution' DeBruijnPattern
rho
          let (UnifyState
s'', Substitution' DeBruijnPattern
sigma) = Int
-> Term
-> UnifyState
-> (UnifyState, Substitution' DeBruijnPattern)
solveEq Int
k (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u) UnifyState
s'
          Substitution' DeBruijnPattern -> UnifyM ()
tellUnifyProof Substitution' DeBruijnPattern
sigma
          UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s''
          -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
          -- Unifies <$> liftTCM (reduce s'')
    Maybe TCErr
Nothing -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [Telescope -> Type -> Int -> Term -> Modality -> UnificationFailure
UnifyUnusableModality (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u Modality
mod]
solutionStep RetryNormalised
_ UnifyState
_ UnifyStep
_ = UnifyM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unify :: UnifyState -> UnifyStrategy -> UnifyM (UnificationResult' UnifyState)
unify :: UnifyState
-> UnifyStrategy -> UnifyM (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
                   then UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s
                   else ListT TCM UnifyStep -> UnifyM (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyStrategy
strategy UnifyState
s)
  where
    tryUnifyStepsAndContinue :: ListT TCM UnifyStep -> UnifyM (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue :: ListT TCM UnifyStep -> UnifyM (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT TCM UnifyStep
steps = do
      UnificationResult' UnifyState
x <- (UnifyStep
 -> UnifyM (UnificationResult' UnifyState)
 -> UnifyM (UnificationResult' UnifyState))
-> UnifyM (UnificationResult' UnifyState)
-> ListT (WriterT UnifyOutput TCM) UnifyStep
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT UnifyStep
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
tryUnifyStep UnifyM (UnificationResult' UnifyState)
forall a. UnifyM (UnificationResult' a)
failure (ListT (WriterT UnifyOutput TCM) UnifyStep
 -> UnifyM (UnificationResult' UnifyState))
-> ListT (WriterT UnifyOutput TCM) UnifyStep
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ (forall a1. TCM a1 -> WriterT UnifyOutput TCM a1)
-> ListT TCM UnifyStep -> ListT (WriterT UnifyOutput TCM) UnifyStep
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a1. TCM a1 -> WriterT UnifyOutput TCM a1
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ListT TCM UnifyStep
steps
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'   -> UnifyState
-> UnifyStrategy -> UnifyM (UnificationResult' UnifyState)
unify UnifyState
s' UnifyStrategy
strategy
        NoUnify NegativeUnification
err  -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify NegativeUnification
err
        DontKnow [UnificationFailure]
err -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow [UnificationFailure]
err

    tryUnifyStep :: UnifyStep
                 -> UnifyM (UnificationResult' UnifyState)
                 -> UnifyM (UnificationResult' UnifyState)
    tryUnifyStep :: UnifyStep
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step UnifyM (UnificationResult' UnifyState)
fallback = do
      Telescope -> UnifyM () -> UnifyM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
        String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"trying unifyStep" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyStep
step
      UnificationResult' UnifyState
x <- UnifyState -> UnifyStep -> UnifyM (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'   -> do
          String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"unifyStep successful."
          String -> Int -> TCM Doc -> UnifyM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCM Doc -> UnifyM ()) -> TCM Doc -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"new unifyState:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
s'
          UnifyLogEntry -> UnifyM ()
writeUnifyLog (UnifyLogEntry -> UnifyM ()) -> UnifyLogEntry -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnifyStep -> UnifyLogEntry
UnificationStep UnifyState
s UnifyStep
step
          UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        NoUnify{}     -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        DontKnow [UnificationFailure]
err1 -> do
          UnificationResult' UnifyState
y <- UnifyM (UnificationResult' UnifyState)
fallback
          case UnificationResult' UnifyState
y of
            DontKnow [UnificationFailure]
err2 -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow ([UnificationFailure] -> UnificationResult' UnifyState)
-> [UnificationFailure] -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ [UnificationFailure]
err1 [UnificationFailure]
-> [UnificationFailure] -> [UnificationFailure]
forall a. [a] -> [a] -> [a]
++ [UnificationFailure]
err2
            UnificationResult' UnifyState
_             -> UnificationResult' UnifyState
-> UnifyM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y

    failure :: UnifyM (UnificationResult' a)
    failure :: UnifyM (UnificationResult' a)
failure = UnificationResult' a -> UnifyM (UnificationResult' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' a -> UnifyM (UnificationResult' a))
-> UnificationResult' a -> UnifyM (UnificationResult' a)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' a
forall a. [UnificationFailure] -> UnificationResult' a
DontKnow []

-- | Turn a term into a pattern binding as many of the given forced variables as possible (in
--   non-forced positions).
patternBindingForcedVars :: (HasConstInfo m, MonadReduce m) => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars :: IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars IntMap Modality
forced Term
v = do
  let v' :: Term
v' = Term -> Term
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ Term
v
  WriterT (IntMap Modality) m DeBruijnPattern
-> m (DeBruijnPattern, IntMap Modality)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (StateT
  (IntMap Modality) (WriterT (IntMap Modality) m) DeBruijnPattern
-> IntMap Modality -> WriterT (IntMap Modality) m DeBruijnPattern
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Modality
-> Term
-> StateT
     (IntMap Modality) (WriterT (IntMap Modality) m) DeBruijnPattern
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(MonadWriter (IntMap Modality) (t (t m)), HasConstInfo (t (t m)),
 DeBruijn a, MonadTrans t, MonadTrans t, Monad (t m), MonadReduce m,
 MonadState (IntMap Modality) (t (t m))) =>
Modality -> Term -> t (t m) (Pattern' a)
go Modality
defaultModality Term
v') IntMap Modality
forced)
  where
    noForced :: a -> f Bool
noForced a
v = IntSet -> Bool
IntSet.null (IntSet -> Bool) -> (IntMap a -> IntSet) -> IntMap a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> IntSet -> IntSet
IntSet.intersection (a -> IntSet
forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
v) (IntSet -> IntSet) -> (IntMap a -> IntSet) -> IntMap a -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap a -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (IntMap a -> Bool) -> f (IntMap a) -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (IntMap a)
forall s (m :: * -> *). MonadState s m => m s
get

    bind :: a -> Int -> m (Pattern' a)
bind a
md Int
i = do
      Just a
md' <- (IntMap a -> Maybe a) -> m (Maybe a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((IntMap a -> Maybe a) -> m (Maybe a))
-> (IntMap a -> Maybe a) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i
      if a -> PartialOrdering -> a -> Bool
forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
related a
md PartialOrdering
POLE a
md'    -- The new binding site must be more relevant (more relevant = smaller).
        then do                 -- The forcing analysis guarantees that there exists such a position.
          IntMap a -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell   (IntMap a -> m ()) -> IntMap a -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> a -> IntMap a
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i a
md
          (IntMap a -> IntMap a) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntMap a -> IntMap a) -> m ()) -> (IntMap a -> IntMap a) -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> IntMap a -> IntMap a
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
i
          Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ a -> Pattern' a
forall a. a -> Pattern' a
varP (Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i)
        else Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])

    go :: Modality -> Term -> t (t m) (Pattern' a)
go Modality
md Term
v = t (t m) Bool
-> t (t m) (Pattern' a)
-> t (t m) (Pattern' a)
-> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> t (t m) Bool
forall (f :: * -> *) a a.
(PrecomputeFreeVars a, MonadState (IntMap a) f) =>
a -> f Bool
noForced Term
v) (Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v) (t (t m) (Pattern' a) -> t (t m) (Pattern' a))
-> t (t m) (Pattern' a) -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ do
      Term
v' <- t m Term -> t (t m) Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m Term -> t (t m) Term) -> t m Term -> t (t m) Term
forall a b. (a -> b) -> a -> b
$ m Term -> t m Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Term -> t m Term) -> m Term -> t m Term
forall a b. (a -> b) -> a -> b
$ Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      case Term
v' of
        Var Int
i [] -> Modality -> Int -> t (t m) (Pattern' a)
forall a (m :: * -> *) a.
(MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
 DeBruijn a, MonadFail m) =>
a -> Int -> m (Pattern' a)
bind Modality
md Int
i  -- we know i is forced
        Con ConHead
c ConInfo
ci Elims
es
          | Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
            [IsForced]
fs <- Definition -> [IsForced]
defForced (Definition -> [IsForced])
-> t (t m) Definition -> t (t m) [IsForced]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> t (t m) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
            let goArg :: IsForced -> f Term -> t (t m) (f (Named name (Pattern' a)))
goArg IsForced
Forced    f Term
v = f (Named name (Pattern' a))
-> t (t m) (f (Named name (Pattern' a)))
forall (m :: * -> *) a. Monad m => a -> m a
return (f (Named name (Pattern' a))
 -> t (t m) (f (Named name (Pattern' a))))
-> f (Named name (Pattern' a))
-> t (t m) (f (Named name (Pattern' a)))
forall a b. (a -> b) -> a -> b
$ (Term -> Named name (Pattern' a))
-> f Term -> f (Named name (Pattern' a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern' a -> Named name (Pattern' a)
forall a name. a -> Named name a
unnamed (Pattern' a -> Named name (Pattern' a))
-> (Term -> Pattern' a) -> Term -> Named name (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Pattern' a
forall a. Term -> Pattern' a
dotP) f Term
v
                goArg IsForced
NotForced f Term
v = (Pattern' a -> Named name (Pattern' a))
-> f (Pattern' a) -> f (Named name (Pattern' a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' a -> Named name (Pattern' a)
forall a name. a -> Named name a
unnamed (f (Pattern' a) -> f (Named name (Pattern' a)))
-> t (t m) (f (Pattern' a))
-> t (t m) (f (Named name (Pattern' a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> t (t m) (Pattern' a))
-> f Term -> t (t m) (f (Pattern' a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Modality -> Term -> t (t m) (Pattern' a)
go (Modality -> Term -> t (t m) (Pattern' a))
-> Modality -> Term -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Modality
md Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<> f Term -> Modality
forall a. LensModality a => a -> Modality
getModality f Term
v) f Term
v
            ([Arg (Named NamedName (Pattern' a))]
ps, IntMap Modality
bound) <- t (t m) [Arg (Named NamedName (Pattern' a))]
-> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (t (t m) [Arg (Named NamedName (Pattern' a))]
 -> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality))
-> t (t m) [Arg (Named NamedName (Pattern' a))]
-> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality)
forall a b. (a -> b) -> a -> b
$ (IsForced
 -> Arg Term -> t (t m) (Arg (Named NamedName (Pattern' a))))
-> [IsForced]
-> Args
-> t (t m) [Arg (Named NamedName (Pattern' a))]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM IsForced
-> Arg Term -> t (t m) (Arg (Named NamedName (Pattern' a)))
forall (f :: * -> *) name.
(Traversable f, LensModality (f Term)) =>
IsForced -> f Term -> t (t m) (f (Named name (Pattern' a)))
goArg ([IsForced]
fs [IsForced] -> [IsForced] -> [IsForced]
forall a. [a] -> [a] -> [a]
++ IsForced -> [IsForced]
forall a. a -> [a]
repeat IsForced
NotForced) Args
vs
            if IntMap Modality -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Modality
bound
              then Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v  -- bound nothing
              else do
                let cpi :: ConPatternInfo
cpi = (ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ci) { conPRecord :: Bool
conPRecord = Bool
True,
                                                  conPLazy :: Bool
conPLazy   = Bool
True } -- Not setting conPType. Is this a problem?
                Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ ConHead
-> ConPatternInfo
-> [Arg (Named NamedName (Pattern' a))]
-> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi ([Arg (Named NamedName (Pattern' a))] -> Pattern' a)
-> [Arg (Named NamedName (Pattern' a))] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (Arg (Named NamedName (Pattern' a))
 -> Arg (Named NamedName (Pattern' a)))
-> [Arg (Named NamedName (Pattern' a))]
-> [Arg (Named NamedName (Pattern' a))]
forall a b. (a -> b) -> [a] -> [b]
map (Origin
-> Arg (Named NamedName (Pattern' a))
-> Arg (Named NamedName (Pattern' a))
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) [Arg (Named NamedName (Pattern' a))]
ps
          | Bool
otherwise -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v   -- Higher constructor (es has IApply)

        -- Non-pattern positions
        Var Int
_ (Elim' Term
_:Elims
_) -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Lam{}       -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Pi{}        -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Def{}       -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        MetaV{}     -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Sort{}      -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Level{}     -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        DontCare{}  -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Dummy{}     -> Pattern' a -> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Lit{}       -> t (t m) (Pattern' a)
forall a. HasCallStack => a
__IMPOSSIBLE__