{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

-- | 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* @UnifyStuck 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'(..)
  , NoLeftInv(..)
  , unifyIndices'
  , unifyIndices ) where

import Prelude hiding (null)

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

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

import qualified Agda.Benchmarking as Bench

import Agda.Interaction.Options (optInjectiveTypeConstructors)

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

import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Constraints ()
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Patterns.Match as Match
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Records

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

import Agda.Utils.Benchmark
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
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.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 @
  )

type FullUnificationResult = UnificationResult'
  ( Telescope                  -- @tel@
  , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
  , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
  , Either NoLeftInv (Substitution, Substitution) -- (τ,leftInv)
  )

data UnificationResult' a
  = Unifies  a                        -- ^ Unification succeeded.
  | NoUnify  NegativeUnification      -- ^ Terms are not unifiable.
  | UnifyBlocked Blocker              -- ^ Unification got blocked on a metavariable
  | UnifyStuck   [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
$cshowsPrec :: forall a. Show a => Int -> UnificationResult' a -> ShowS
showsPrec :: Int -> UnificationResult' a -> ShowS
$cshow :: forall a. Show a => UnificationResult' a -> String
show :: UnificationResult' a -> String
$cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
showList :: [UnificationResult' a] -> ShowS
Show, (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
$cfmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
fmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
$c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
Functor, (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
$cfold :: forall m. Monoid m => UnificationResult' m -> m
fold :: forall m. Monoid m => UnificationResult' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$ctoList :: forall a. UnificationResult' a -> [a]
toList :: forall a. UnificationResult' a -> [a]
$cnull :: forall a. UnificationResult' a -> Bool
null :: forall a. UnificationResult' a -> Bool
$clength :: forall a. UnificationResult' a -> Int
length :: forall a. UnificationResult' a -> Int
$celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
$cmaximum :: forall a. Ord a => UnificationResult' a -> a
maximum :: forall a. Ord a => UnificationResult' a -> a
$cminimum :: forall a. Ord a => UnificationResult' a -> a
minimum :: forall a. Ord a => UnificationResult' a -> a
$csum :: forall a. Num a => UnificationResult' a -> a
sum :: forall a. Num a => UnificationResult' a -> a
$cproduct :: forall a. Num a => UnificationResult' a -> a
product :: forall a. Num a => UnificationResult' a -> a
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'
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
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
  :: (PureTCM m, MonadBench m, BenchPhase m ~ Bench.Phase, MonadError TCErr m)
  => Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope       -- ^ @gamma@
  -> FlexibleVars    -- ^ @flex@
  -> Type            -- ^ @a@
  -> Args            -- ^ @us@
  -> Args            -- ^ @vs@
  -> m UnificationResult
unifyIndices :: forall (m :: * -> *).
(PureTCM m, MonadBench m, BenchPhase m ~ Phase,
 MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m UnificationResult
unifyIndices Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs =
  Account (BenchPhase m)
-> m UnificationResult -> m UnificationResult
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase m
Phase
Bench.Typing, BenchPhase m
Phase
Bench.CheckLHS, BenchPhase m
Phase
Bench.UnifyIndices] (m UnificationResult -> m UnificationResult)
-> m UnificationResult -> m UnificationResult
forall a b. (a -> b) -> a -> b
$
    ((Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
  Either NoLeftInv (Substitution, Substitution))
 -> (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern]))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
      Either NoLeftInv (Substitution, Substitution))
-> UnificationResult
forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Telescope
a,PatternSubstitution
b,[NamedArg DeBruijnPattern]
c,Either NoLeftInv (Substitution, Substitution)
_) -> (Telescope
a,PatternSubstitution
b,[NamedArg DeBruijnPattern]
c)) (UnificationResult'
   (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
    Either NoLeftInv (Substitution, Substitution))
 -> UnificationResult)
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
-> m UnificationResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs

unifyIndices'
  :: (PureTCM m, MonadError TCErr m)
  => Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope     -- ^ @gamma@
  -> FlexibleVars  -- ^ @flex@
  -> Type          -- ^ @a@
  -> Args          -- ^ @us@
  -> Args          -- ^ @vs@
  -> m FullUnificationResult
unifyIndices' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [] [] = UnificationResult'
  (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
   Either NoLeftInv (Substitution, Substitution))
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult'
   (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
    Either NoLeftInv (Substitution, Substitution))
 -> m (UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
          Either NoLeftInv (Substitution, Substitution))))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
      Either NoLeftInv (Substitution, Substitution))
-> m (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
         Either NoLeftInv (Substitution, Substitution)))
forall a b. (a -> b) -> a -> b
$ (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
 Either NoLeftInv (Substitution, Substitution))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern],
      Either NoLeftInv (Substitution, Substitution))
forall a. a -> UnificationResult' a
Unifies (Telescope
tel, PatternSubstitution
forall a. Substitution' a
idS, [], (Substitution, Substitution)
-> Either NoLeftInv (Substitution, Substitution)
forall a b. b -> Either a b
Right (Substitution
forall a. Substitution' a
idS, Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs = do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"unifyIndices"
          , (TCMT IO Doc
"tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
          , (TCMT IO Doc
"flex =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO 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
          , (TCMT IO Doc
"a    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a)
          , (TCMT IO Doc
"us   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
us
          , (TCMT IO Doc
"vs   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
vs
          ]
    initialState    <- Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
forall (m :: * -> *).
PureTCM m =>
Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs
    reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState
    (result,log) <- runUnifyLogT $ unify initialState rightToLeftStrategy
    forM result $ \ UnifyState
s -> do -- Unifies case
        let output :: UnifyOutput
output = [UnifyOutput] -> UnifyOutput
forall a. Monoid a => [a] -> a
mconcat [UnifyOutput
output | (UnificationStep UnifyState
_ UnifyStep
_ UnifyOutput
output,UnifyState
_) <- UnifyLog
log ]
        let ps :: [NamedArg DeBruijnPattern]
ps = Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
output) ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (UnifyState -> Telescope
eqTel UnifyState
initialState)
        tauInv <- do
          strict     <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
          cubicalCompatible <- cubicalCompatibleOption
          withoutK <- withoutKOption
          case linv of
            Just NoLeftInv
reason -> Either NoLeftInv (Substitution, Substitution)
-> m (Either NoLeftInv (Substitution, Substitution))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
reason)
            Maybe NoLeftInv
Nothing
              | Bool
strict            -> Either NoLeftInv (Substitution, Substitution)
-> m (Either NoLeftInv (Substitution, Substitution))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
SplitOnStrict)
              | Bool
cubicalCompatible -> UnifyState
-> UnifyLog -> m (Either NoLeftInv (Substitution, Substitution))
forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyState
-> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse UnifyState
initialState UnifyLog
log
              | Bool
withoutK          -> Either NoLeftInv (Substitution, Substitution)
-> m (Either NoLeftInv (Substitution, Substitution))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
NoCubical)
              | Bool
otherwise         -> Either NoLeftInv (Substitution, Substitution)
-> m (Either NoLeftInv (Substitution, Substitution))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
WithKEnabled)
        reportSDoc "tc.lhs.unify" 20 $ "ps:" <+> pretty ps
        return $ (varTel s, unifySubst output, ps, tauInv)



type UnifyStrategy = forall m. (PureTCM m, MonadPlus m) => UnifyState -> m 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 =
    [m UnifyStep] -> m UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Int] -> (Int -> m UnifyStep) -> [m 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 -> m UnifyStep) -> [m UnifyStep])
-> (Int -> m UnifyStep) -> [m 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 = [m UnifyStep] -> m UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m UnifyStep] -> m UnifyStep) -> [m UnifyStep] -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ ((Int -> UnifyState -> m UnifyStep) -> m UnifyStep)
-> [Int -> UnifyState -> m UnifyStep] -> [m UnifyStep]
forall a b. (a -> b) -> [a] -> [b]
map (\Int -> UnifyState -> m UnifyStep
strat -> Int -> UnifyState -> m UnifyStep
strat Int
k UnifyState
s) ([Int -> UnifyState -> m UnifyStep] -> [m UnifyStep])
-> [Int -> UnifyState -> m UnifyStep] -> [m UnifyStep]
forall a b. (a -> b) -> a -> b
$
-- ASR (2021-02-07). The below eta-expansions are required by GHC >=
-- 9.0.1 (see Issue #4955).
    [ (\Int
n -> Int -> UnifyStrategy
skipIrrelevantStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
basicUnifyStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
literalStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
dataStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
etaExpandVarStrategy  Int
n)
    , (\Int
n -> Int -> UnifyStrategy
etaExpandEquationStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
injectiveTypeConStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
injectivePragmaStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
simplifySizesStrategy Int
n)
    , (\Int
n -> Int -> UnifyStrategy
checkEqualityStrategy Int
n)
    ]

-- | @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 a) => Int -> a -> Maybe a
isHom :: forall a. (Free a, Subst a) => 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 a. 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 a. Subst 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 = (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{unDom = a} u v <- Equality -> m Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s)
    -- Andreas, 2019-02-23: reduce equality for the sake of isHom?
  ha <- fromMaybeMP $ isHom n a
  (mi, mj) <- addContext (varTel s) $ (,) <$> isEtaVar u ha <*> isEtaVar v ha
  reportSDoc "tc.lhs.unify" 30 $ "isEtaVar results: " <+> text (show [mi,mj])
  case (mi, mj) of
    (Just Int
i, Just Int
j)
     | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j -> m UnifyStep
forall a. m a
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 :: m UnifyStep
firstTryLeft  = [m UnifyStep] -> m UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fi Term
v Either () ()
forall {b}. Either () b
left)
                                , UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fj Term
u Either () ()
forall {a}. Either a ()
right)]
           firstTryRight :: m UnifyStep
firstTryRight = [m UnifyStep] -> m UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fj Term
u Either () ()
forall {a}. Either a ()
right)
                                , UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fi Term
v Either () ()
forall {b}. Either () b
left)]
       String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fi = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fi)
       String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fj = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fj)
       String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"chooseFlex: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexChoice -> String
forall a. Show a => a -> String
show FlexChoice
choice)
       case FlexChoice
choice of
         FlexChoice
ChooseLeft   -> m UnifyStep
firstTryLeft
         FlexChoice
ChooseRight  -> m UnifyStep
firstTryRight
         FlexChoice
ExpandBoth   -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- This should be taken care of by etaExpandEquationStrategy
         FlexChoice
ChooseEither -> m UnifyStep
firstTryRight
    (Just Int
i, Maybe Int
_)
     | Just FlexibleVar Int
fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex -> UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fi Term
v Either () ()
forall {b}. Either () b
left
    (Maybe Int
_, Just Int
j)
     | Just FlexibleVar Int
fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
j FlexibleVars
flex -> UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ Int
-> Dom Type -> FlexibleVar Int -> Term -> Either () () -> UnifyStep
Solution Int
k Dom Type
dom{unDom = ha} FlexibleVar Int
fj Term
u Either () ()
forall {a}. Either a ()
right
    (Maybe Int, Maybe Int)
_ -> m UnifyStep
forall a. m a
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
    left :: Either () b
left = () -> Either () b
forall a b. a -> Either a b
Left (); right :: Either a ()
right = () -> Either a ()
forall a b. b -> Either a b
Right ()

dataStrategy :: Int -> UnifyStrategy
dataStrategy :: Int -> UnifyStrategy
dataStrategy Int
k UnifyState
s = do
  Equal Dom{unDom = a} u v <- Equality -> m Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm (Equality -> m Equality) -> m Equality -> m Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Equality -> m Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> m Equality) -> m Equality -> m Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> UnifyState -> m Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s
  sortOk <- reduce (getSort a) <&> \case
    Type{} -> Bool
True
    Inf{}  -> Bool
True
    SSet{} -> Bool
True
    Sort
_      -> Bool
False
  case unEl a of
    Def QName
d Elims
es | Bool
sortOk -> do
      npars <- m (Maybe Int) -> m Int
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (m (Maybe Int) -> m Int) -> m (Maybe Int) -> m Int
forall a b. (a -> b) -> a -> b
$ QName -> m (Maybe Int)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
getNumberOfParameters QName
d
      let (pars,ixs) = splitAt npars $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
      reportSDoc "tc.lhs.unify" 40 $ addContext (varTel s `abstract` eqTel s) $
        "Found equation at datatype " <+> prettyTCM d
         <+> " with parameters " <+> prettyTCM (raise (size (eqTel s) - k) pars)
      case (u, 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 -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep -> m UnifyStep
forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i Term
v (m UnifyStep -> m UnifyStep) -> m UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep -> m UnifyStep
forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
j Term
u (m UnifyStep -> m UnifyStep) -> m UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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)
_ -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> m UnifyStep
forall a. m a
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
        (_ , u) <- IntSet -> a -> m (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 flexRigOccurrenceIn i u of
          Just FlexRig
StronglyRigid -> m b
ret
          Maybe FlexRig
_ -> m b
forall a. m a
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
  ha <- Maybe Type -> m Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> m Type) -> Maybe Type -> m Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Maybe Type
forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n Type
a
  return $ Deletion k ha u 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 = a} u v <- Equality -> m Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> m Equality) -> Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
  ha <- fromMaybeMP $ isHom n a
  (u, v) <- reduce (u, v)
  case (u , v) of
    (Lit Literal
l1 , Lit Literal
l2)
     | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2  -> UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Literal -> Literal -> UnifyStep
LitConflict Int
k Type
ha Literal
l1 Literal
l2
    (Term, Term)
_ -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy Int
k UnifyState
s = do
  Equal Dom{unDom = a} u v <- Equality -> m Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> m Equality) -> m Equality -> m Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> UnifyState -> m Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
k UnifyState
s
  shouldEtaExpand u v a s `mplus` shouldEtaExpand v u a 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
      fi       <- Maybe (FlexibleVar Int) -> m (FlexibleVar Int)
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe (FlexibleVar Int) -> m (FlexibleVar Int))
-> Maybe (FlexibleVar Int) -> m (FlexibleVar Int)
forall a b. (a -> b) -> a -> b
$ Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i (UnifyState -> FlexibleVars
flexVars UnifyState
s)
      reportSDoc "tc.lhs.unify" 50 $
        "Found flexible variable " <+> text (show 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.
      let k  = 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 -- position of var i in telescope
          b0 = 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 Int
k UnifyState
s
      b         <- addContext (telFromList $ take k $ telToList $ varTel s) $ reduce b0
      (d, pars) <- catMaybesMP $ isEtaRecordType b
      ps        <- fromMaybeMP $ allProjElims es
      guard =<< orM
        [ pure $ not $ null ps
        , isRecCon v  -- is the other term a record constructor?
        , (Right True ==) <$> runBlocked (isSingletonRecord d pars)
        ]
      reportSDoc "tc.lhs.unify" 50 $
        "with projections " <+> prettyTCM (map snd ps)
      reportSDoc "tc.lhs.unify" 50 $
        "at record type " <+> prettyTCM d
      return $ EtaExpandVar fi d pars
    shouldEtaExpand Term
_ Term
_ Type
_ UnifyState
_ = m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    isRecCon :: Term -> f Bool
isRecCon (Con ConHead
c ConInfo
_ Elims
_) = Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, RecordData) -> Bool)
-> f (Maybe (QName, RecordData)) -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (ConHead -> QName
conName ConHead
c)
    isRecCon Term
_           = Bool -> f Bool
forall a. a -> f a
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 = a} u v <- Int -> UnifyState -> m Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s
  (d, pars) <- catMaybesMP $ addContext tel $ isEtaRecordType a
  guard =<< orM
    [ (Right True ==) <$> runBlocked (isSingletonRecord d pars)
    , shouldProject u
    , shouldProject v
    ]
  return $ EtaExpandEquation k d pars
  where
    shouldProject :: PureTCM m => Term -> m Bool
    shouldProject :: forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject = \case
      Def QName
f Elims
es   -> QName -> m Bool
forall (m :: * -> *).
(HasConstInfo m, HasBuiltins m) =>
QName -> m Bool
usesCopatterns QName
f
      Con ConHead
c ConInfo
_ Elims
_  -> Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, RecordData) -> Bool)
-> m (Maybe (QName, RecordData)) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (ConHead -> QName
conName ConHead
c)

      Var Int
_ Elims
_    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Lam ArgInfo
_ Abs Term
_    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit Literal
_      -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Pi Dom Type
_ Abs Type
_     -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort Sort
_     -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level Level
_    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV MetaId
_ Elims
_  -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      DontCare Term
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Dummy String
s Elims
_  -> String -> m 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` ListTel -> Telescope
telFromList (Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
take Int
k (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> ListTel) -> Telescope -> ListTel
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s)

simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy Int
k UnifyState
s = do
  isSizeName <- m (QName -> Bool)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTest
  Equal Dom{unDom = a} u v <- getReducedEquality k s
  case unEl a of
    Def QName
d Elims
_ -> do
      Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> Bool
isSizeName QName
d
      su <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
      sv <- sizeView v
      case (su, sv) of
        (SizeSuc Term
u, SizeSuc Term
v) -> UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m 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 -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeView, SizeView)
_ -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy Int
k UnifyState
s = do
  injTyCon <- PragmaOptions -> Bool
optInjectiveTypeConstructors (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  guard injTyCon
  eq <- eqUnLevel =<< getReducedEquality k s
  case 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
      def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      guard $ case theDef 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
                PrimitiveSort{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                GeneralizableVar{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                Constructor{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Never a type!
      let 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 -> 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'
      return $ TypeConInjectivity k d us vs
    Equality
_ -> m UnifyStep
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy Int
k UnifyState
s = do
  eq <- Equality -> m Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> m Equality) -> m Equality -> m Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> UnifyState -> m Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
k UnifyState
s
  case 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
      def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      guard $ defInjective def
      let 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 -> 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'
      return $ TypeConInjectivity k d us vs
    Equality
_ -> m UnifyStep
forall a. m a
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
  Telescope -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ())
-> (Either Blocker Bool -> Bool) -> Either Blocker Bool -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) (Either Blocker Bool -> m ()) -> m (Either Blocker Bool) -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BlockT m Bool -> m (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Dom Type -> BlockT m Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom Type
a)  -- reduction takes place here
  -- TODO: do something in case the above is blocked (i.e. `Left b`)
  UnifyStep -> m UnifyStep
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
forall a b. (a -> b) -> a -> b
$ Int -> UnifyStep
SkipIrrelevantEquation Int
k


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

unifyStep
  :: (PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m)
  => UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m) =>
UnifyState -> UnifyStep -> m (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
    isReflexive <- Telescope -> m (Either Blocker Bool) -> m (Either Blocker Bool)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m (Either Blocker Bool) -> m (Either Blocker Bool))
-> m (Either Blocker Bool) -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ BlockT m Bool -> m (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT m Bool -> m (Either Blocker Bool))
-> BlockT m Bool -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> BlockT m Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v
    withoutK <- withoutKOption
    splitOnStrict <- asksTC envSplitOnStrict
    case isReflexive of
      Left Blocker
block   -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
      Right Bool
False  -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
      Right Bool
True | Bool
withoutK Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
splitOnStrict
                   -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Term -> UnificationFailure
UnifyReflexiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Term
u]
      Right Bool
True   -> do
        let (UnifyState
s', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k Term
u UnifyState
s
        PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
        UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> m UnifyState -> m (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> m Telescope) -> UnifyState -> m UnifyState
Lens' UnifyState Telescope
lensEqTel Telescope -> m Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce UnifyState
s'

unifyStep UnifyState
s step :: UnifyStep
step@Solution{} = RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (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
  m Bool
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT (QName -> m Bool) -> QName -> m Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (m (UnificationResult' UnifyState)
 -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
  withoutK <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption

  -- Split equation telescope into parts before and after current equation
  let (eqListTel1, _ : eqListTel2) = splitAt k $ telToList $ eqTel s
      (eqTel1, eqTel2) = (telFromList eqListTel1, telFromList eqListTel2)

  -- Get constructor telescope and target indices
  cdef  <- getConInfo c
  let ctype  = Definition -> Type
defType Definition
cdef Type -> Args -> Type
`piApply` Args
pars
  addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
    "Constructor type: " <+> prettyTCM ctype
  TelV ctel ctarget <- addContext (varTel s `abstract` eqTel1) $ telView ctype
  let 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 a. [a] -> 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
  dtype    <- (`piApply` pars) . defType <$> getConstInfo d
  addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
    "Datatype type: " <+> prettyTCM 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
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
      notforced = Int -> IsForced -> [IsForced]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
hduTel) IsForced
NotForced

  -- The left inverse computed here is not actually used when computing
  -- a left inverse for the overall match, so as a slight optimisation
  -- we just don't bother computing it. __IMPOSSIBLE__ because that
  -- field in the result is never evaluated.
  res <- addContext (varTel s) $ unifyIndices' (Just __IMPOSSIBLE__)
           hduTel
           (allFlexVars notforced hduTel)
           (raise (size ctel) dtype)
           (raise (size ctel) ixs)
           cixs
  case 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
_ -> m (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Higher-dimensional unification is blocked: propagate
    UnifyBlocked Blocker
block -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block

    -- 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.
    UnifyStuck [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 :: PatternSubstitution
rho1    = Int -> PatternSubstitution
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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: PatternSubstitution
rho3    = DeBruijnPattern -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
ceq PatternSubstitution
rho1
          eqTel2' :: Telescope
eqTel2' = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: PatternSubstitution
rho     = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel2) PatternSubstitution
rho3

      PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho

      eqTel' <- Telescope -> m Telescope -> m Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Telescope -> m Telescope) -> m Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> m 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
      (lhs', rhs') <- addContext (varTel s) $ do
        let ps = Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg [NamedArg DeBruijnPattern])
rho ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (Telescope -> [NamedArg DeBruijnPattern])
-> Telescope -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
        (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
        case (lhsMatch, rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> (Args, Args) -> m (Args, Args)
forall a. a -> m a
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)
_ -> m (Args, Args)
forall a. HasCallStack => a
__IMPOSSIBLE__

      return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }


    UnifyStuck [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 -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [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 a. Subst a => Int -> a -> a
raise Int
n Term
u) (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
n Term
v) (Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
k) Args
ixs)]

    Unifies (Telescope
eqTel1', PatternSubstitution
rho0, [NamedArg DeBruijnPattern]
_, Either NoLeftInv (Substitution, Substitution)
_) -> do
      -- Split ps0 into parts for eqTel1 and ctel
      let (PatternSubstitution
rho1, PatternSubstitution
rho2) = Int
-> PatternSubstitution
-> (PatternSubstitution, PatternSubstitution)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ctel) PatternSubstitution
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' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg [NamedArg DeBruijnPattern])
rho2 ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: PatternSubstitution
rho3    = DeBruijnPattern -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
ceq PatternSubstitution
rho1
          eqTel2' :: Telescope
eqTel2' = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: PatternSubstitution
rho     = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
eqTel2) PatternSubstitution
rho3

      PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho

      eqTel' <- Telescope -> m Telescope -> m Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Telescope -> m Telescope) -> m Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> m 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
      (lhs', rhs') <- addContext (varTel s) $ do
        let ps = Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg [NamedArg DeBruijnPattern])
rho ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (Telescope -> [NamedArg DeBruijnPattern])
-> Telescope -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
        (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
        case (lhsMatch, rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> (Args, Args) -> m (Args, Args)
forall a. a -> m a
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)
_ -> m (Args, Args)
forall a. HasCallStack => a
__IMPOSSIBLE__

      return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = 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
      m Bool
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT (QName -> m Bool) -> QName -> m Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (m (UnificationResult' UnifyState)
 -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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
_ -> m (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
      m Bool
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT (QName -> m Bool) -> QName -> m Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (m (UnificationResult' UnifyState)
 -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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
_ -> m (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
  recd <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> m (Maybe RecordData) -> m RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
d
  let delta = RecordData -> Telescope
_recTel RecordData
recd Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
      c     = RecordData -> ConHead
_recConHead RecordData
recd
  let nfields         = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta
      (varTel', rho)  = expandTelescopeVar (varTel s) (m-1-i) delta c
      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
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j) | Int
j <- [Int
0 .. Int
nfields Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ]
  tellUnifySubst $ rho
  return $ Unifies $ UState
    { varTel   = varTel'
    , flexVars = projectFlexible ++ liftFlexibles nfields (flexVars s)
    , eqTel    = applyPatSubst rho $ eqTel s
    , eqLHS    = applyPatSubst rho $ eqLHS s
    , eqRHS    = applyPatSubst rho $ eqRHS 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

    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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar 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
  recd  <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> m (Maybe RecordData) -> m RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
d
  let delta = RecordData -> Telescope
_recTel RecordData
recd Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
      c     = RecordData -> ConHead
_recConHead RecordData
recd
  lhs   <- expandKth $ eqLHS s
  rhs   <- expandKth $ eqRHS s
  let (tel, sigma) = expandTelescopeVar (eqTel s) k delta c
  tellUnifyProof sigma
  Unifies <$> do
   lensEqTel reduce $ s
    { eqTel    = tel
    , eqLHS    = lhs
    , eqRHS    = 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
      vs <- (Telescope, Args) -> Args
forall a b. (a, b) -> b
snd ((Telescope, Args) -> Args) -> m (Telescope, Args) -> m Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Args -> Term -> m (Telescope, Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m) =>
QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord QName
d Args
pars (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v)
      vs <- reduce vs
      return $ us1 ++ vs ++ 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 -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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
  sizeTy <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  sizeSu <- sizeSuc 1 (var 0)
  let n          = UnifyState -> Int
eqCount UnifyState
s
      sub        = Int -> Substitution -> Substitution
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 -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Term -> Substitution -> Substitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
sizeSu (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1
      eqFlatTel  = Telescope -> [Dom Type]
forall a. TermSubst 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' = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom Type])
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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
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'     = [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!
  return $ Unifies $ s
    { eqTel = eqTel'
    , eqLHS = updateAt k (const $ defaultArg u) $ eqLHS s
    , eqRHS = updateAt k (const $ defaultArg v) $ eqRHS s
    }

unifyStep UnifyState
s (SkipIrrelevantEquation Int
k) = do
  let lhs :: Args
lhs = UnifyState -> Args
eqLHS UnifyState
s
      (UnifyState
s', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
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
  PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
  UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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
  dtype <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  TelV dtel _ <- telView dtype
  let deq = QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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...
  Unifies <$> do
   lensEqTel reduce $ s
    { eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq)
    , eqLHS = us ++ dropAt k (eqLHS s)
    , eqRHS = vs ++ dropAt k (eqRHS 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
$c== :: RetryNormalised -> RetryNormalised -> Bool
== :: RetryNormalised -> RetryNormalised -> Bool
$c/= :: RetryNormalised -> RetryNormalised -> Bool
/= :: 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
$cshowsPrec :: Int -> RetryNormalised -> ShowS
showsPrec :: Int -> RetryNormalised -> ShowS
$cshow :: RetryNormalised -> String
show :: RetryNormalised -> String
$cshowList :: [RetryNormalised] -> ShowS
showList :: [RetryNormalised] -> ShowS
Show)

solutionStep
  :: (PureTCM m, MonadWriter UnifyOutput m)
  => RetryNormalised
  -> UnifyState
  -> UnifyStep
  -> m (UnificationResult' UnifyState)
solutionStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (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.
  inMakeCase <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eMakeCase
  let 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 ]
  (p, bound) <- patternBindingForcedVars forcedVars u

  -- To maintain the invariant that each variable in varTel is bound exactly once in the pattern
  -- substitution we need to turn the bound variables in `p` into dot patterns in the rest of the
  -- substitution.
  let dotSub = (PatternSubstitution -> PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution
-> [PatternSubstitution]
-> PatternSubstitution
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS PatternSubstitution
forall a. Substitution' a
idS [ Int -> DeBruijnPattern -> PatternSubstitution
forall a. EndoSubst 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 (returned by
  -- patternBindingForcedVars).
  let 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        = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ (Int -> Dom (String, Type) -> Dom (String, Type))
-> [Int] -> ListTel -> ListTel
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom (String, Type) -> Dom (String, Type)
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 -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
        where
          upd :: Int -> Dom (String, Type) -> Dom (String, Type)
upd Int
i Dom (String, Type)
a | Just Modality
md' <- Int -> IntMap Modality -> Maybe Modality
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Modality
vars = Modality -> Dom (String, Type) -> Dom (String, Type)
forall a. LensModality a => Modality -> a -> a
setModality (Modality -> Modality -> Modality
composeModality Modality
md Modality
md') Dom (String, Type)
a
                  | Bool
otherwise                        = Dom (String, Type)
a
  s <- return $ s { varTel = updModality (getModality fi) bound (varTel s) }

  reportSDoc "tc.lhs.unify.force" 45 $ vcat
    [ "forcedVars =" <+> pretty (IntMap.keys forcedVars)
    , "u          =" <+> prettyTCM u
    , "p          =" <+> prettyTCM p
    , "bound      =" <+> pretty (IntMap.keys bound)
    , "dotSub     =" <+> pretty 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{ unDom = a' } = getVarType (m-1-i) s
  equalTypes <- addContext (varTel s) $ runBlocked $ do
    reportSDoc "tc.lhs.unify" 45 $ "Equation type: " <+> prettyTCM a
    reportSDoc "tc.lhs.unify" 45 $ "Variable type: " <+> prettyTCM a'
    pureEqualType a 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.
  envmod <- currentModality
  let eqrel  = Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom
      eqmod  = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom
      varmod = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom'
      mod    = Bool -> (Modality -> Modality) -> Modality -> Modality
forall b a. IsBool b => b -> (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
$ Bool -> (Modality -> Modality) -> Modality -> Modality
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Modality -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity Modality
envmod) (Quantity -> Modality -> Modality
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity)
             (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Modality
varmod
  reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom)
  reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod
  reportSDoc "tc.lhs.unify" 65 $ text $ "Solution must be usable in a " ++ show mod ++ " 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.
  -- Andrea, 2020-10-15: It looks at meta instantiations now.
  eusable <- addContext (varTel s) $ runExceptT $ usableMod mod u
  caseEitherM (return eusable) (return . UnifyBlocked) $ \ Bool
usable -> do

  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Modality ok: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
usable
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
usable (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Rejected solution: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM 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 -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [] else do

  case Either Blocker Bool
equalTypes of
    Left Blocker
block  -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
    Right Bool
False -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
    Right Bool
True | Bool
usable ->
      case Int
-> DeBruijnPattern
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution)
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, PatternSubstitution)
Nothing | RetryNormalised
retry RetryNormalised -> RetryNormalised -> Bool
forall a. Eq a => a -> a -> Bool
== RetryNormalised
RetryNormalised -> do
          u <- Term -> m Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
u
          s <- lensVarTel normalise s
          solutionStep DontRetryNormalised s step{ solutionTerm = u }
        Maybe (UnifyState, PatternSubstitution)
Nothing ->
          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Int -> Term -> UnificationFailure
UnifyRecursiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u]
        Just (UnifyState
s', PatternSubstitution
sub) -> do
          let rho :: PatternSubstitution
rho = PatternSubstitution
sub PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` PatternSubstitution
dotSub
          PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
rho
          let (UnifyState
s'', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Term
u) UnifyState
s'
          PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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'')
    Right Bool
True -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Int -> Term -> Modality -> UnificationFailure
UnifyUnusableModality (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u Modality
mod]
solutionStep RetryNormalised
_ UnifyState
_ UnifyStep
_ = m (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unify
  :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
  => UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
                   then UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s
                   else ListT m UnifyStep -> m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyState -> ListT m UnifyStep
UnifyStrategy
strategy UnifyState
s)
  where
    tryUnifyStepsAndContinue
      :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
      => ListT m UnifyStep -> m (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT m UnifyStep
steps = do
      x <- (UnifyStep
 -> m (UnificationResult' UnifyState)
 -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
-> ListT m UnifyStep
-> m (UnificationResult' UnifyState)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep m (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure ListT m UnifyStep
steps
      case x of
        Unifies UnifyState
s'     -> UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s' UnifyState -> m UnifyStep
UnifyStrategy
strategy
        NoUnify NegativeUnification
err    -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify NegativeUnification
err
        UnifyBlocked Blocker
b -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b
        UnifyStuck [UnificationFailure]
err -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [UnificationFailure]
err

    tryUnifyStep :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
                 => UnifyStep
                 -> m (UnificationResult' UnifyState)
                 -> m (UnificationResult' UnifyState)
    tryUnifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step m (UnificationResult' UnifyState)
fallback = do
      Telescope -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying unifyStep" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM UnifyStep
step
      (x, output) <- WriterT UnifyOutput m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState, UnifyOutput)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT UnifyOutput m (UnificationResult' UnifyState)
 -> m (UnificationResult' UnifyState, UnifyOutput))
-> WriterT UnifyOutput m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyState
-> UnifyStep
-> WriterT UnifyOutput m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m) =>
UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
      case x of
        Unifies UnifyState
s'   -> do
          String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unifyStep successful."
          String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"new unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
s'
          -- tell output
          (UnifyLogEntry, UnifyState) -> m ()
forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog ((UnifyLogEntry, UnifyState) -> m ())
-> (UnifyLogEntry, UnifyState) -> m ()
forall a b. (a -> b) -> a -> b
$ (UnifyState -> UnifyStep -> UnifyOutput -> UnifyLogEntry
UnificationStep UnifyState
s UnifyStep
step UnifyOutput
output,UnifyState
s')
          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        NoUnify{}       -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        UnifyBlocked Blocker
b1 -> do
          y <- m (UnificationResult' UnifyState)
fallback
          case y of
            UnifyStuck [UnificationFailure]
_    -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b1
            UnifyBlocked Blocker
b2 -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked (Blocker -> UnificationResult' UnifyState)
-> Blocker -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b1 Blocker
b2
            UnificationResult' UnifyState
_               -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
        UnifyStuck [UnificationFailure]
err1 -> do
          y <- m (UnificationResult' UnifyState)
fallback
          case y of
            UnifyStuck [UnificationFailure]
err2 -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck ([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 -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y

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

-- | Turn a term into a pattern while binding as many of the given forced variables as possible (in
--   non-forced positions).
patternBindingForcedVars :: PureTCM m => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars :: forall (m :: * -> *).
PureTCM m =>
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}.
(HasConstInfo (t (t m)), DeBruijn a,
 MonadWriter (IntMap Modality) (t (t m)),
 MonadState (IntMap Modality) (t (t m)), MonadTrans t, MonadTrans t,
 Monad (t m), MonadReduce m) =>
Modality -> Term -> t (t m) (Pattern' a)
go Modality
unitModality Term
v') IntMap Modality
forced)
  where
    noForced :: a -> m Bool
noForced a
v = (IntMap a -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((IntMap a -> Bool) -> m Bool) -> (IntMap a -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
IntSet.disjoint (a -> IntSet
forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
v) (IntSet -> Bool) -> (IntMap a -> IntSet) -> IntMap a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap a -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet

    bind :: a -> Int -> m (Pattern' a)
bind a
md Int
i = do
      (IntMap a -> Maybe a) -> m (Maybe a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i) m (Maybe a) -> (Maybe a -> m (Pattern' a)) -> m (Pattern' a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just a
md' | a -> PartialOrdering -> a -> Bool
forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
related a
md PartialOrdering
POLE a
md' -> do
          -- The new binding site must be more relevant (more relevant = smaller).
          -- "The forcing analysis guarantees that there exists such a position."
          -- Really? Andreas, 2021-08-18, issue #5506
          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 a. a -> m 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)
        Maybe a
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m 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 {a} {m :: * -> *} {a}.
(MonadState (IntMap a) m, PrecomputeFreeVars a) =>
a -> m Bool
noForced Term
v) (Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) 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
      v' <- t m Term -> t (t m) Term
forall (m :: * -> *) a. Monad m => m a -> t m a
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 (m :: * -> *) a. Monad m => m a -> t m a
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 v' of
        Var Int
i [] -> Modality -> Int -> t (t m) (Pattern' a)
forall {m :: * -> *} {a} {a}.
(MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
 DeBruijn a) =>
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
            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
Forced    Arg Term
v = NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a)))
-> NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
forall a b. (a -> b) -> a -> b
$ (Term -> Named NamedName (Pattern' a))
-> Arg Term -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed (Pattern' a -> Named NamedName (Pattern' a))
-> (Term -> Pattern' a) -> Term -> Named NamedName (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Pattern' a
forall a. Term -> Pattern' a
dotP) Arg Term
v
                goArg IsForced
NotForced Arg Term
v = (Pattern' a -> Named NamedName (Pattern' a))
-> Arg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed (Arg (Pattern' a) -> NamedArg (Pattern' a))
-> t (t m) (Arg (Pattern' a)) -> t (t m) (NamedArg (Pattern' a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> t (t m) (Pattern' a))
-> Arg Term -> t (t m) (Arg (Pattern' a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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 -> Modality -> Modality
composeModality Modality
md (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Arg Term -> Modality
forall a. LensModality a => a -> Modality
getModality Arg Term
v) Arg Term
v
            (ps, bound) <- listen $ zipWithM goArg (fs ++ repeat NotForced) vs
            if IntMap.null bound
              then return $ dotP v  -- bound nothing
              else do
                let cpi = (ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ci) { conPLazy   = True } -- Not setting conPType. Is this a problem?
                return $ ConP c cpi $ map (setOrigin Inserted) ps
          | Bool
otherwise -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) 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
_:Elims
_) -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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{}       -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) 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
          -- Andreas, 2023-08-20, issue #6767
          -- The last case is not __IMPOSSIBLE__ (regresssion in 2.6.2).
          -- It would be if we had reduced to `constructorForm`,
          -- however, turning a `LitNat` into constructors would only result in churn,
          -- since literals have no variables that could be bound.