{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.With where

import Prelude hiding ((!!))

import Control.Monad.Writer (WriterT, runWriterT, tell)

import qualified Data.List as List
import Data.Maybe
import Data.Foldable ( foldrM )
import Data.Semigroup ( sconcat )

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Info
import Agda.Syntax.Position

import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive ( getRefl )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..))
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Warnings ( warning )

import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (empty)
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | Split pattern variables according to with-expressions.

--   Input:
--
--   [@Δ@]         context of types and with-arguments.
--
--   [@Δ ⊢ t@]     type of rhs.
--
--   [@Δ ⊢ vs : as@]    with arguments and their types
--
--   Output:
--
--   [@Δ₁@]              part of context needed for with arguments and their types.
--
--   [@Δ₂@]              part of context not needed for with arguments and their types.
--
--   [@π@]               permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
--
--   [@Δ₁Δ₂ ⊢ t'@]       type of rhs under @π@
--
--   [@Δ₁ ⊢ vs' : as'@]  with-arguments and their types depending only on @Δ₁@.

splitTelForWith
  -- Input:
  :: Telescope                         -- ^ __@Δ@__             context of types and with-arguments.
  -> Type                              -- ^ __@Δ ⊢ t@__         type of rhs.
  -> List1 (Arg (Term, EqualityView))  -- ^ __@Δ ⊢ vs : as@__   with arguments and their types.
  -- Output:
  -> ( Telescope                         -- @Δ₁@             part of context needed for with arguments and their types.
     , Telescope                         -- @Δ₂@             part of context not needed for with arguments and their types.
     , Permutation                       -- @π@              permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
     , Type                              -- @Δ₁Δ₂ ⊢ t'@      type of rhs under @π@
     , List1 (Arg (Term, EqualityView))  -- @Δ₁ ⊢ vs' : as'@ with- and rewrite-arguments and types under @π@.
     )              -- ^ (__@Δ₁@__,__@Δ₂@__,__@π@__,__@t'@__,__@vtys'@__) where
--
--   [@Δ₁@]        part of context needed for with arguments and their types.
--
--   [@Δ₂@]        part of context not needed for with arguments and their types.
--
--   [@π@]         permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
--
--   [@Δ₁Δ₂ ⊢ t'@] type of rhs under @π@
--
--   [@Δ₁ ⊢ vtys'@]  with-arguments and their types under @π@.

splitTelForWith :: Telescope
-> Type
-> List1 (Arg (Term, EqualityView))
-> (Telescope, Telescope, Permutation, Type,
    List1 (Arg (Term, EqualityView)))
splitTelForWith Telescope
delta Type
t List1 (Arg (Term, EqualityView))
vtys = let
    -- Split the telescope into the part needed to type the with arguments
    -- and all the other stuff.
    fv :: VarSet
fv = List1 (Arg (Term, EqualityView)) -> VarSet
forall t. Free t => t -> VarSet
allFreeVars List1 (Arg (Term, EqualityView))
vtys
    SplitTel Telescope
delta1 Telescope
delta2 Permutation
perm = VarSet -> Telescope -> SplitTel
splitTelescope VarSet
fv Telescope
delta

    -- Δ₁Δ₂ ⊢ π : Δ
    pi :: Substitution' Term
pi = Impossible -> Permutation -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm)
    -- Δ₁ ⊢ ρ : Δ₁Δ₂  (We know that as does not depend on Δ₂.)
    rho :: Substitution' Term
rho = Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Int -> Substitution' Term) -> Int -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
    -- Δ₁ ⊢ ρ ∘ π : Δ
    rhopi :: Substitution' Term
rhopi = Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' Term
rho Substitution' Term
pi

    -- We need Δ₁Δ₂ ⊢ t'
    t' :: Type
t' = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
pi Type
t
    -- and Δ₁ ⊢ vtys'
    vtys' :: List1 (Arg (Term, EqualityView))
vtys' = Substitution' (SubstArg (List1 (Arg (Term, EqualityView))))
-> List1 (Arg (Term, EqualityView))
-> List1 (Arg (Term, EqualityView))
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (List1 (Arg (Term, EqualityView))))
rhopi List1 (Arg (Term, EqualityView))
vtys

  in (Telescope
delta1, Telescope
delta2, Permutation
perm, Type
t', List1 (Arg (Term, EqualityView))
vtys')


-- | Abstract with-expressions @vs@ to generate type for with-helper function.
--
-- Each @EqualityType@, coming from a @rewrite@, will turn into 2 abstractions.

withFunctionType
  :: Telescope                          -- ^ @Δ₁@                        context for types of with-expressions.
  -> List1 (Arg (Term, EqualityView))   -- ^ @Δ₁,Δ₂ ⊢ vs : raise Δ₂ as@  with and rewrite-expressions and their type.
  -> Telescope                          -- ^ @Δ₁ ⊢ Δ₂@                   context extension to type with-expressions.
  -> Type                               -- ^ @Δ₁,Δ₂ ⊢ b@                 type of rhs.
  -> Boundary                           -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b@ boundary of rhs.
  -> TCM (Type, (Nat1, Nat))
    -- ^ @Δ₁ → wtel → Δ₂′ → b′@ such that
    --     @[vs/wtel]wtel = as@ and
    --     @[vs/wtel]Δ₂′ = Δ₂@ and
    --     @[vs/wtel]b′ = b@.
    -- Plus the final number of with-arguments and the number of visible ones.
withFunctionType :: Telescope
-> List1 (Arg (Term, EqualityView))
-> Telescope
-> Type
-> Boundary
-> TCM (Type, (Int, Int))
withFunctionType Telescope
delta1 List1 (Arg (Term, EqualityView))
vtys Telescope
delta2 Type
b Boundary
bndry = Telescope -> TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int))
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
delta1 (TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int)))
-> TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int))
forall a b. (a -> b) -> a -> b
$ do

  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.abstract" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"preparing for with-abstraction"

  -- Normalize and η-contract the type @b@ of the rhs and the types @delta2@
  -- of the pattern variables not mentioned in @vs : as@.
  let dbg :: Int -> [Char] -> a -> m ()
dbg Int
n [Char]
s a
x = [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.abstract" Int
n (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x

  Type
d2b <- Telescope -> Type -> Boundary -> TCM Type
telePiPath_ Telescope
delta2 Type
b Boundary
bndry
  Int -> [Char] -> Type -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
Int -> [Char] -> a -> m ()
dbg Int
30 [Char]
"Δ₂ → B" Type
d2b
  Type
d2b  <- Type -> TCM Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
d2b
  Int -> [Char] -> Type -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
Int -> [Char] -> a -> m ()
dbg Int
30 [Char]
"normal Δ₂ → B" Type
d2b
  Type
d2b  <- Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Type
d2b
  Int -> [Char] -> Type -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
Int -> [Char] -> a -> m ()
dbg Int
30 [Char]
"eta-contracted Δ₂ → B" Type
d2b

  List1 (Arg (Term, EqualityView))
vtys <- List1 (Arg (Term, EqualityView))
-> TCMT IO (List1 (Arg (Term, EqualityView)))
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract (List1 (Arg (Term, EqualityView))
 -> TCMT IO (List1 (Arg (Term, EqualityView))))
-> TCMT IO (List1 (Arg (Term, EqualityView)))
-> TCMT IO (List1 (Arg (Term, EqualityView)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< List1 (Arg (Term, EqualityView))
-> TCMT IO (List1 (Arg (Term, EqualityView)))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise List1 (Arg (Term, EqualityView))
vtys

  -- wd2b = wtel → [vs : as] (Δ₂ → B)
  Type
wd2b <- (Arg (Term, EqualityView) -> Type -> TCM Type)
-> Type -> List1 (Arg (Term, EqualityView)) -> TCM Type
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Arg (Term, EqualityView) -> Type -> TCM Type
piAbstract Type
d2b List1 (Arg (Term, EqualityView))
vtys
  Int -> [Char] -> Type -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
Int -> [Char] -> a -> m ()
dbg Int
30 [Char]
"wΓ → Δ₂ → B" Type
wd2b

  let nwithargs :: Int
nwithargs = NonEmpty EqualityView -> Int
forall (f :: * -> *).
(Functor f, Foldable f) =>
f EqualityView -> Int
countWithArgs (NonEmpty EqualityView -> Int) -> NonEmpty EqualityView -> Int
forall a b. (a -> b) -> a -> b
$ (Arg (Term, EqualityView) -> EqualityView)
-> List1 (Arg (Term, EqualityView)) -> NonEmpty EqualityView
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (Arg (Term, EqualityView) -> (Term, EqualityView))
-> Arg (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg) List1 (Arg (Term, EqualityView))
vtys
  let nwithpats :: Int
nwithpats = List1 (Arg (Term, EqualityView)) -> Int
forall (f :: * -> *).
(Functor f, Foldable f) =>
f (Arg (Term, EqualityView)) -> Int
countWithPats List1 (Arg (Term, EqualityView))
vtys

  TelV Telescope
wtel Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
nwithargs Type
wd2b

  -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂"
  let bndry' :: Boundary
bndry' = [(Int, (Term, Term))] -> Boundary
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary [(Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sd2,(Term -> Term
lams Term
u0, Term -> Term
lams Term
u1)) | (Int
i,(Term
u0,Term
u1)) <- Boundary -> [(Int, (Term, Term))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary Boundary
bndry, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
sd2]
        where sd2 :: Int
sd2 = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
              lams :: Term -> Term
lams = Telescope -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs Telescope
wtel (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
delta2

  Type
d1wd2b <- Telescope -> Type -> Boundary -> TCM Type
telePiPath_ Telescope
delta1 Type
wd2b Boundary
bndry'

  Int -> [Char] -> Type -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadDebug m, PrettyTCM a) =>
Int -> [Char] -> a -> m ()
dbg Int
30 [Char]
"Δ₁ → wΓ → Δ₂ → B" Type
d1wd2b

  (Type, (Int, Int)) -> TCM (Type, (Int, Int))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
d1wd2b, (Int
nwithargs, Int
nwithpats))

-- | Count the number of arguments introduced into the type of the with-function.
countWithArgs :: (Functor f, Foldable f) => f EqualityView -> Nat1
countWithArgs :: forall (f :: * -> *).
(Functor f, Foldable f) =>
f EqualityView -> Int
countWithArgs = f Int -> Int
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (f Int -> Int)
-> (f EqualityView -> f Int) -> f EqualityView -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EqualityView -> Int) -> f EqualityView -> f Int
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Int
forall {a}. Num a => EqualityView -> a
countArgs
  where
    countArgs :: EqualityView -> a
countArgs OtherType{}    = a
1
    countArgs IdiomType{}    = a
2
    countArgs EqualityType{} = a
2

-- | Count the number of with-patterns in the with-clause
--   that need to be transformed to regular patterns
--   in the **current round** of with-abstraction
--   (important for nested with).
countWithPats :: (Functor f, Foldable f) => f (Arg (Term, EqualityView)) -> Nat1
countWithPats :: forall (f :: * -> *).
(Functor f, Foldable f) =>
f (Arg (Term, EqualityView)) -> Int
countWithPats = f Int -> Int
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (f Int -> Int)
-> (f (Arg (Term, EqualityView)) -> f Int)
-> f (Arg (Term, EqualityView))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg (Term, EqualityView) -> Int)
-> f (Arg (Term, EqualityView)) -> f Int
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap \case
    -- Andreas, 2025-04-08, see issue #7788.
    Arg ArgInfo
ai (Term
_, OtherType   {}) -> if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai then Int
1 else Int
0
      -- A hidden @with@ (issue #500) does not have a with-pattern in the abstract syntax.
    Arg ArgInfo
ai (Term
_, IdiomType   {}) -> if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai then Int
2 else Int
1
      -- The hidden version of the inspect idiom has just one with-pattern in the abstract syntax.
    Arg ArgInfo
ai (Term
_, EqualityType{}) -> if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai then Int
2 else Int
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- The desugaring of @rewrite@ produces two new with-patterns in the abstract syntax.
      -- They are always @NotHidden@.


-- | From a list of @with@ and @rewrite@ expressions and their types,
--   compute the list of final @with@ expressions (after expanding the @rewrite@s).
withArguments :: List1 (Arg (Term, EqualityView)) ->
                 TCM (List1 (Arg Term))
withArguments :: List1 (Arg (Term, EqualityView)) -> TCM (List1 (Arg Term))
withArguments List1 (Arg (Term, EqualityView))
vtys = do
  NonEmpty (List1 (Arg Term)) -> List1 (Arg Term)
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (List1 (Arg Term)) -> List1 (Arg Term))
-> TCMT IO (NonEmpty (List1 (Arg Term))) -> TCM (List1 (Arg Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    List1 (Arg (Term, EqualityView))
-> (Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
-> TCMT IO (NonEmpty (List1 (Arg Term)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 (Arg (Term, EqualityView))
vtys ((Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
 -> TCMT IO (NonEmpty (List1 (Arg Term))))
-> (Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
-> TCMT IO (NonEmpty (List1 (Arg Term)))
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info (Term, EqualityView)
ts) -> do
      (Term -> Arg Term) -> NonEmpty Term -> List1 (Arg Term)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info) (NonEmpty Term -> List1 (Arg Term))
-> TCMT IO (NonEmpty Term) -> TCM (List1 (Arg Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        case (Term, EqualityView)
ts of
          (Term
v, OtherType Type
a) -> do
            NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty Term -> TCMT IO (NonEmpty Term))
-> NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ Term -> NonEmpty Term
forall el coll. Singleton el coll => el -> coll
singleton Term
v
          (Term
prf, eqt :: EqualityView
eqt@(EqualityType Range
_r Sort
_s QName
_eq Args
_pars Arg Term
_t Arg Term
v Arg Term
_v')) -> do
            NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty Term -> TCMT IO (NonEmpty Term))
-> NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v Term -> [Term] -> NonEmpty Term
forall a. a -> [a] -> NonEmpty a
:| Term
prf Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: []
          (Term
v, IdiomType Type
t) -> do
            Arg Term -> Term
mkRefl <- TCM (Arg Term -> Term)
getRefl
            NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty Term -> TCMT IO (NonEmpty Term))
-> NonEmpty Term -> TCMT IO (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ Term
v Term -> [Term] -> NonEmpty Term
forall a. a -> [a] -> NonEmpty a
:| Arg Term -> Term
mkRefl (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: []

-- | Compute the clauses for the with-function given the original patterns.
buildWithFunction
  :: [Name]               -- ^ Names of the module parameters of the parent function.
  -> QName                -- ^ Name of the parent function.
  -> QName                -- ^ Name of the with-function.
  -> Type                 -- ^ Types of the parent function.
  -> Telescope            -- ^ Context of parent patterns.
  -> [NamedArg DeBruijnPattern] -- ^ Parent patterns.
  -> Nat                  -- ^ Number of module parameters in parent patterns
  -> Substitution         -- ^ Substitution from parent lhs to with function lhs
  -> Permutation          -- ^ Final permutation.
  -> Nat                  -- ^ Number of needed vars.
  -> Nat                  -- ^ Number of with expressions.
  -> List1 A.SpineClause  -- ^ With-clauses.
  -> TCM (List1 A.SpineClause) -- ^ With-clauses flattened wrt. parent patterns.
buildWithFunction :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Substitution' Term
-> Permutation
-> Int
-> Int
-> List1 (Clause' SpineLHS)
-> TCM (List1 (Clause' SpineLHS))
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Substitution' Term
withSub Permutation
perm Int
n1 Int
n List1 (Clause' SpineLHS)
cs = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> List1 (Clause' SpineLHS) -> TCM (List1 (Clause' SpineLHS))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause List1 (Clause' SpineLHS)
cs
  where
    -- Nested with-functions will iterate this function once for each parent clause.
    buildWithClause :: Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause (A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
allPs) [ProblemEq]
inheritedPats RHS
rhs WhereDeclarations
wh Catchall
catchall) = do
      let ([NamedArg Pattern]
ps, [NamedArg Pattern]
wps)    = [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
splitOffTrailingWithPatterns [NamedArg Pattern]
allPs
          ([NamedArg Pattern]
wps0, [NamedArg Pattern]
wps1) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
wps
          ps0 :: [NamedArg Pattern]
ps0          = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> Pattern
forall {e}. Pattern' e -> Pattern' e
fromWithP) [NamedArg Pattern]
wps0
            where
            fromWithP :: Pattern' e -> Pattern' e
fromWithP (A.WithP PatInfo
_ Pattern' e
p) = Pattern' e
p
            fromWithP Pattern' e
_ = Pattern' e
forall a. HasCallStack => a
__IMPOSSIBLE__

      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.split" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
vcat
        [ TCMT IO Doc
"buildWithClause"
        , 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
$ TCMT IO Doc
"n    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
n
        , 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
$ TCMT IO Doc
"wps  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Pattern] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
wps
        , 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
$ TCMT IO Doc
"wps0 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Pattern] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
wps0
        , 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
$ TCMT IO Doc
"wps1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Pattern] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
wps1
        ]

      -- Andreas, 2025-04-07, issue #7759
      -- Usually the following is impossible because the with-clause collection
      -- already looks for the correct number of with-patterns.
      -- However, if the lhs is just an ellipsis, we can slip through the cracks.
      -- Thus, we install another check here to enforce the correct number of with-patterns.
      Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when ([NamedArg Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Pattern]
wps0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        SpineLHS -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange SpineLHS
lhs (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
TooFewPatternsInWithClause

      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inheritedPats:" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p 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 (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
v 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
        | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats
        ]
      ([ProblemEq]
strippedPats, [NamedArg Pattern]
ps') <- [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"strippedPats:" Int
2 (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, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p 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 (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
v 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
t)
                                       | A.ProblemEq Pattern
p Term
v Dom Type
t <- [ProblemEq]
strippedPats ]
      RHS
rhs <- [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
strippedPats RHS
rhs
      let ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n1 [NamedArg Pattern]
ps'
      let result :: Clause' SpineLHS
result = SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux ([NamedArg Pattern] -> SpineLHS) -> [NamedArg Pattern] -> SpineLHS
forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
ps1 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps0 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps2 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
wps1)
                     ([ProblemEq]
inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
                     RHS
rhs WhereDeclarations
wh Catchall
catchall
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
vcat
        [ TCMT IO Doc
"buildWithClause returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Clause' SpineLHS -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Clause' SpineLHS
result
        ]
      Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Clause' SpineLHS
result

    buildRHS :: [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
_ rhs :: RHS
rhs@A.RHS{}                 = RHS -> TCMT IO RHS
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
    buildRHS [ProblemEq]
_ rhs :: RHS
rhs@RHS
A.AbsurdRHS             = RHS -> TCMT IO RHS
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
    buildRHS [ProblemEq]
_ (A.WithRHS QName
q List1 WithExpr
es List1 Clause
cs)         = QName -> List1 WithExpr -> List1 Clause -> RHS
A.WithRHS QName
q List1 WithExpr
es (List1 Clause -> RHS) -> TCMT IO (List1 Clause) -> TCMT IO RHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      (Clause -> TCMT IO Clause)
-> List1 Clause -> TCMT IO (List1 Clause)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM ((Clause' SpineLHS -> Clause
forall a b. LHSToSpine a b => b -> a
A.spineToLhs (Clause' SpineLHS -> Clause)
-> (Clause' SpineLHS -> Clause' SpineLHS)
-> Clause' SpineLHS
-> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots) (Clause' SpineLHS -> Clause)
-> (Clause -> TCMT IO (Clause' SpineLHS))
-> Clause
-> TCMT IO Clause
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> (Clause -> Clause' SpineLHS)
-> Clause
-> TCMT IO (Clause' SpineLHS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Clause' SpineLHS
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine) List1 Clause
cs
    buildRHS [ProblemEq]
strippedPats1 (A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
strippedPats2 RHS
rhs WhereDeclarations
wh) =
      (RHS -> WhereDeclarations -> RHS)
-> WhereDeclarations -> RHS -> RHS
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [ProblemEq])
withSub ([ProblemEq] -> [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a b. (a -> b) -> a -> b
$ [ProblemEq]
strippedPats1 [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats2)) WhereDeclarations
wh (RHS -> RHS) -> TCMT IO RHS -> TCMT IO RHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [] RHS
rhs

    -- The stripped patterns computed by buildWithClause lives in the context
    -- of the top with-clause (of the current call to buildWithFunction). When
    -- we recurse we expect inherited patterns to live in the context
    -- of the innermost parent clause. Note that this makes them live in the
    -- context of the with-function arguments before any pattern matching. We
    -- need to update again once the with-clause patterns have been checked.
    -- This happens in Rules.Def.checkClause before calling checkRHS.
    permuteNamedDots :: A.SpineClause -> A.SpineClause
    permuteNamedDots :: Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots (A.Clause SpineLHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Catchall
catchall) =
      SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
A.Clause SpineLHS
lhs (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [ProblemEq])
withSub [ProblemEq]
strippedPats) RHS
rhs WhereDeclarations
wh Catchall
catchall


-- The arguments of @stripWithClausePatterns@ are documented
-- at its type signature.
-- The following is duplicate information, but may help reading the examples below.
--
-- [@Δ@]   context bound by lhs of original function.
-- [@f@]   name of @with@-function.
-- [@t@]   type of the original function.
-- [@qs@]  internal patterns for original function.
-- [@np@]  number of module parameters in @qs@
-- [@π@]   permutation taking @vars(qs)@ to @support(Δ)@.
-- [@ps@]  patterns in with clause (eliminating type @t@).
-- [@ps'@] patterns for with function (presumably of type @Δ@).

{-| @stripWithClausePatterns cxtNames parent f t Δ qs np π ps = ps'@

Example:

@
  record Stream (A : Set) : Set where
    coinductive
    constructor delay
    field       force : A × Stream A

  record SEq (s t : Stream A) : Set where
    coinductive
    field
      ~force : let a , as = force s
                   b , bs = force t
               in  a ≡ b × SEq as bs

  test : (s : Nat × Stream Nat) (t : Stream Nat) → SEq (delay s) t → SEq t (delay s)
  ~force (test (a     , as) t p) with force t
  ~force (test (suc n , as) t p) | b , bs = ?
@

With function:

@
  f : (t : Stream Nat) (w : Nat × Stream Nat) (a : Nat) (as : Stream Nat)
      (p : SEq (delay (a , as)) t) → (fst w ≡ a) × SEq (snd w) as

  Δ  = t a as p   -- reorder to bring with-relevant (= needed) vars first
  π  = a as t p → Δ
  qs = (a     , as) t p ~force
  ps = (suc n , as) t p ~force
  ps' = (suc n) as t p
@

Resulting with-function clause is:

@
  f t (b , bs) (suc n) as t p
@

Note: stripWithClausePatterns factors __@ps@__ through __@qs@__, thus

@
  ps = qs[ps']
@

where @[..]@ is to be understood as substitution.
The projection patterns have vanished from __@ps'@__ (as they are already in __@qs@__).
-}

stripWithClausePatterns
  :: [Name]                   -- ^ __@cxtNames@__ names of the module parameters of the parent function
  -> QName                    -- ^ __@parent@__ name of the parent function.
  -> QName                    -- ^ __@f@__   name of with-function.
  -> Type                     -- ^ __@t@__   top-level type of the original function.
  -> Telescope                -- ^ __@Δ@__   context of patterns of parent function.
  -> [NamedArg DeBruijnPattern] -- ^ __@qs@__  internal patterns for original function.
  -> Nat                      -- ^ __@npars@__ number of module parameters in @qs@.
  -> Permutation              -- ^ __@π@__   permutation taking @vars(qs)@ to @support(Δ)@.
  -> [NamedArg A.Pattern]     -- ^ __@ps@__  patterns in with clause (eliminating type @t@).
  -> TCM ([A.ProblemEq], [NamedArg A.Pattern]) -- ^ __@ps'@__ patterns for with function (presumably of type @Δ@).
stripWithClausePatterns :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
parent QName
f Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps = do
  -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074)
  [NamedArg Pattern]
ps <- [NamedArg Pattern] -> TCM [NamedArg Pattern]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg Pattern]
ps
  -- Ulf, 2016-11-16 Issue 2303: We need the module parameter
  -- instantiations from qs, so we make sure
  -- that t is the top-level type of the parent function and add patterns for
  -- the module parameters to ps before stripping.
  let paramPat :: Int -> DeBruijnPattern -> Pattern
paramPat Int
i DeBruijnPattern
_ = BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName (Name -> BindName) -> Name -> BindName
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Int -> Name
forall a. a -> [a] -> Int -> a
indexWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ [Name]
cxtNames Int
i
      ps' :: [NamedArg Pattern]
ps' = (Int -> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [Int] -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
 -> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> (Int
    -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> Int
-> NamedArg DeBruijnPattern
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> Pattern)
-> Named NamedName DeBruijnPattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> Pattern)
 -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> (Int -> DeBruijnPattern -> Pattern)
-> Int
-> Named NamedName DeBruijnPattern
-> Named NamedName Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DeBruijnPattern -> Pattern
paramPat) [Int
0..] (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
take Int
npars [NamedArg DeBruijnPattern]
qs) [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps
  [NamedArg Pattern]
psi <- ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps' Type
t
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
vcat
    [ TCMT IO Doc
"stripping patterns"
    , 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
$ TCMT IO Doc
"t   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    , 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
$ TCMT IO Doc
"ps  = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
    , 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
$ TCMT IO Doc
"ps' = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps')
    , 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
$ TCMT IO Doc
"psi = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
psi)
    , 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
delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
               TCMT IO Doc
"qs  = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
    , 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
$ TCMT IO Doc
"perm= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
    ]

  -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function!
  ([NamedArg Pattern]
ps', [ProblemEq]
strippedPats) <- WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> TCM ([NamedArg Pattern], [ProblemEq])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
 -> TCM ([NamedArg Pattern], [ProblemEq]))
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> TCM ([NamedArg Pattern], [ProblemEq])
forall a b. (a -> b) -> a -> b
$ Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip (QName -> Elims -> Term
Def QName
parent []) Type
t [NamedArg Pattern]
psi [NamedArg DeBruijnPattern]
qs
  Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([ProblemEq] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProblemEq]
strippedPats) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
$
    TCMT IO Doc
"strippedPats:" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p 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 (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
v 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
strippedPats ]
  let psp :: [NamedArg Pattern]
psp = Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [NamedArg Pattern]
ps'
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
vcat
    [ 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
$ TCMT IO Doc
"ps' = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps')
    , 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
$ TCMT IO Doc
"psp = " 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern] -> [TCMT IO Doc])
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
psp)
    ]
  ([ProblemEq], [NamedArg Pattern])
-> TCM ([ProblemEq], [NamedArg Pattern])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProblemEq]
strippedPats, [NamedArg Pattern]
psp)
  where

    -- We need to get the correct hiding from the lhs context. The unifier may have moved bindings
    -- sites around so we can't trust the hiding of the parent pattern variables. We should preserve
    -- the origin though.
    varArgInfo :: DBPatVar -> ArgInfo
varArgInfo = \ DBPatVar
x -> let n :: Int
n = DBPatVar -> Int
dbPatVarIndex DBPatVar
x in
                        if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [ArgInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgInfo]
infos then [ArgInfo]
infos [ArgInfo] -> Int -> ArgInfo
forall a. HasCallStack => [a] -> Int -> a
!! Int
n else ArgInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
      where infos :: [ArgInfo]
infos = [ArgInfo] -> [ArgInfo]
forall a. [a] -> [a]
reverse ([ArgInfo] -> [ArgInfo]) -> [ArgInfo] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> ArgInfo)
-> [Dom ([Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom ([Char], Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo ([Dom ([Char], Type)] -> [ArgInfo])
-> [Dom ([Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
delta

    setVarArgInfo :: DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p = Origin -> NamedArg Pattern -> NamedArg Pattern
forall a. LensOrigin a => Origin -> a -> a
setOrigin (NamedArg Pattern -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Pattern
p) (NamedArg Pattern -> NamedArg Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NamedArg Pattern -> NamedArg Pattern
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (DBPatVar -> ArgInfo
varArgInfo DBPatVar
x) NamedArg Pattern
p

    strip
      :: Term                         -- Self.
      -> Type                         -- The type to be eliminated.
      -> [NamedArg A.Pattern]         -- With-clause patterns.
      -> [NamedArg DeBruijnPattern]   -- Parent-clause patterns with de Bruijn indices relative to Δ.
      -> WriterT [ProblemEq] TCM [NamedArg A.Pattern]
            -- With-clause patterns decomposed by parent-clause patterns.
            -- Also outputs named dot patterns from the parent clause that
            -- we need to add let-bindings for.

    -- Case: out of with-clause patterns.
    strip :: Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self Type
t [] qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
_ : [NamedArg DeBruijnPattern]
_) = do
      [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
15 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
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
vcat
        [ TCMT IO Doc
"strip (out of A.Patterns)"
        , 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
$ TCMT IO Doc
"qs  =" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
        , 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
$ TCMT IO Doc
"self=" 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
self
        , 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
$ TCMT IO Doc
"t   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]
      -- Andreas, 2015-06-11, issue 1551:
      -- As the type t develops, we need to insert more implicit patterns,
      -- due to copatterns / flexible arity.
      [NamedArg Pattern]
ps <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [] Type
t
      if [NamedArg Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
ps then TypeError -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
TooFewPatternsInWithClause
       else Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self Type
t [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

    -- Case: out of parent-clause patterns.
    -- This is only ok if all remaining with-clause patterns
    -- are implicit patterns (we inserted too many).
    strip Term
_ Type
_ [NamedArg Pattern]
ps      []      = do
      let implicit :: Pattern' e -> Bool
implicit (A.WildP{})     = Bool
True
          implicit (A.ConP ConPatInfo
ci AmbiguousQName
_ NAPs e
_) = ConPatInfo -> ConOrigin
conPatOrigin ConPatInfo
ci ConOrigin -> ConOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== ConOrigin
ConOSystem
          implicit Pattern' e
_               = Bool
False
      Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((NamedArg Pattern -> Bool) -> [NamedArg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern -> Bool
forall {e}. Pattern' e -> Bool
implicit (Pattern -> Bool)
-> (NamedArg Pattern -> Pattern) -> NamedArg Pattern -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps) (WriterT [ProblemEq] (TCMT IO) ()
 -> WriterT [ProblemEq] (TCMT IO) ())
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TypeError -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
TooManyPatternsInWithClause
      [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    -- Case: both parent-clause pattern and with-clause pattern present.
    -- Make sure they match, and decompose into subpatterns.
    strip Term
self Type
t (NamedArg Pattern
p0 : [NamedArg Pattern]
ps) qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
_)
      | A.AsP PatInfo
_ BindName
x Pattern
p <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0 = do
        (Dom Type
a, Abs Type
_) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
        let v :: Term
v = DeBruijnPattern -> Term
patternToTerm (NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
q)
        [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP BindName
x) Term
v Dom Type
a]
        Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self Type
t ((Named NamedName Pattern -> Named NamedName Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern
p Pattern -> Named NamedName Pattern -> Named NamedName Pattern
forall a b. a -> Named NamedName b -> Named NamedName a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg Pattern
p0 NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps) [NamedArg DeBruijnPattern]
qs
    strip Term
self Type
t ps0 :: [NamedArg Pattern]
ps0@(NamedArg Pattern
p0 : [NamedArg Pattern]
ps) qs0 :: [NamedArg DeBruijnPattern]
qs0@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
qs) = do
      NamedArg Pattern
p <- ((Named NamedName Pattern
 -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
-> NamedArg Pattern
-> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
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 ((Named NamedName Pattern
  -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
 -> NamedArg Pattern
 -> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern))
-> ((Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
    -> Named NamedName Pattern
    -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
-> (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
-> NamedArg Pattern
-> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
-> Named NamedName Pattern
-> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern)
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) -> Named NamedName a -> f (Named NamedName b)
traverse) Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern
forall (m :: * -> *).
(MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
Pattern -> m Pattern
expandLitPattern NamedArg Pattern
p0
      [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
15 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
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
vcat
        [ TCMT IO Doc
"strip"
        , 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
$ TCMT IO Doc
"ps0 =" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps0)
        , 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
$ TCMT IO Doc
"exp =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p
        , 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
$ TCMT IO Doc
"qs0 =" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs0)
        , 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
$ TCMT IO Doc
"self=" 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
self
        , 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
$ TCMT IO Doc
"t   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]
      case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
q of
        ProjP ProjOrigin
o QName
d -> case NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p of
          Just (ProjOrigin
o', AmbQ List1 QName
ds) -> do
            -- We assume here that neither @o@ nor @o'@ can be @ProjSystem@.
            Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ProjOrigin
o ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
o') (WriterT [ProblemEq] (TCMT IO) ()
 -> WriterT [ProblemEq] (TCMT IO) ())
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p0 (WriterT [ProblemEq] (TCMT IO) ()
 -> WriterT [ProblemEq] (TCMT IO) ())
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Telescope
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
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
delta do
              [Char] -> Int -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.strip" Int
90 ([Char] -> WriterT [ProblemEq] (TCMT IO) ())
-> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"p0 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ NamedArg Pattern -> [Char]
forall a. Show a => a -> [Char]
show NamedArg Pattern
p0
              [Char] -> Int -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.strip" Int
80 ([Char] -> WriterT [ProblemEq] (TCMT IO) ())
-> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"getRange p0 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (NamedArg Pattern -> Range
forall a. HasRange a => a -> Range
getRange NamedArg Pattern
p0)
              Warning -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> WriterT [ProblemEq] (TCMT IO) ())
-> Warning -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern
-> ProjOrigin -> NamedArg DeBruijnPattern -> ProjOrigin -> Warning
WithClauseProjectionFixityMismatch NamedArg Pattern
p0 ProjOrigin
o' NamedArg DeBruijnPattern
q ProjOrigin
o
            -- Andreas, 2016-12-28, issue #2360:
            -- We disambiguate the projection in the with clause
            -- to the projection in the parent clause.
            QName
d  <- TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM QName -> WriterT [ProblemEq] (TCMT IO) QName)
-> TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
forall a b. (a -> b) -> a -> b
$ QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
            Bool
found <- List1 QName
-> (QName -> WriterT [ProblemEq] (TCMT IO) Bool)
-> WriterT [ProblemEq] (TCMT IO) Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
existsM List1 QName
ds ((QName -> WriterT [ProblemEq] (TCMT IO) Bool)
 -> WriterT [ProblemEq] (TCMT IO) Bool)
-> (QName -> WriterT [ProblemEq] (TCMT IO) Bool)
-> WriterT [ProblemEq] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ \ QName
d' -> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool)
-> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool)
-> (Maybe Projection -> Maybe QName) -> Maybe Projection -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Projection -> QName) -> Maybe Projection -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Projection -> QName
projOrig (Maybe Projection -> Bool)
-> TCMT IO (Maybe Projection) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
d'
            if Bool -> Bool
not Bool
found then WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch else do
              (Term
self1, Type
t1, [NamedArg Pattern]
ps) <- TCM (Term, Type, [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) (Term, Type, [NamedArg Pattern])
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Term, Type, [NamedArg Pattern])
 -> WriterT [ProblemEq] (TCMT IO) (Term, Type, [NamedArg Pattern]))
-> TCM (Term, Type, [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) (Term, Type, [NamedArg Pattern])
forall a b. (a -> b) -> a -> b
$ do
                Type
t <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
                (Dom Type
_, Term
self1, Type
t1) <- (Dom Type, Term, Type)
-> Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type)
forall a. a -> Maybe a -> a
fromMaybe (Dom Type, Term, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type))
-> TCMT IO (Maybe (Dom Type, Term, Type))
-> TCMT IO (Dom Type, Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> Type
-> ProjOrigin
-> QName
-> TCMT IO (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
self Type
t ProjOrigin
o QName
d
                -- Andreas, 2016-01-21, issue #1791
                -- The type of a field might start with hidden quantifiers.
                -- So we may have to insert more implicit patterns here.
                [NamedArg Pattern]
ps <- ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps Type
t1
                (Term, Type, [NamedArg Pattern])
-> TCM (Term, Type, [NamedArg Pattern])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
self1, Type
t1, [NamedArg Pattern]
ps)
              Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self1 Type
t1 [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs
          Maybe (ProjOrigin, AmbiguousQName)
Nothing -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch

        -- We can safely strip dots from variables. The unifier will put them back when required.
        VarP PatternInfo
_ DBPatVar
x | A.DotP PatInfo
_ Expr
u <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p
                 , A.Var Name
y <- Expr -> Expr
unScope Expr
u -> do
          (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x (NamedArg Pattern -> Pattern -> NamedArg Pattern
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName Name
y) NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))

        VarP PatternInfo
_ DBPatVar
x  ->
          (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))

        IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x  ->
          (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))

        DefP{}  -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

        DotP PatternInfo
i Term
v  -> do
          (Dom Type
a, Abs Type
_) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
          [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) Term
v Dom Type
a]
          case Term
v of
            Var Int
x [] | PatOVar{} <- PatternInfo -> PatOrigin
patOrigin PatternInfo
i
               -> (NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var Int
x)
            Term
_  -> (NamedArg Pattern -> NamedArg Pattern
makeWildP NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse Term
v

        q' :: DeBruijnPattern
q'@(ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
qs') -> do
         [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
           TCMT IO Doc
"parent pattern is constructor " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
         (Dom Type
a, Abs Type
b) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
         -- The type of the current pattern is a datatype.
         Def QName
d Elims
es <- TCM Term -> WriterT [ProblemEq] (TCMT IO) Term
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> WriterT [ProblemEq] (TCMT IO) Term)
-> TCM Term -> WriterT [ProblemEq] (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
         let us :: Args
us = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
         -- Get the original constructor and field names.
         ConHead
c <- (SigError -> ConHead)
-> (ConHead -> ConHead) -> Either SigError ConHead -> ConHead
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SigError -> ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__ (ConHead -> ConHead -> ConHead
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` ConHead
c) (Either SigError ConHead -> ConHead)
-> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
-> WriterT [ProblemEq] (TCMT IO) ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TCM (Either SigError ConHead)
-> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Either SigError ConHead)
 -> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead))
-> TCM (Either SigError ConHead)
-> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Either SigError ConHead)
getConForm (QName -> TCM (Either SigError ConHead))
-> QName -> TCM (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c

         case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of

          -- Andreas, 2015-07-07 Issue 1606.
          -- Agda sometimes changes a record of dot patterns into a dot pattern,
          -- so the user should be allowed to do likewise.
          -- Jesper, 2017-11-16. This is now also allowed for data constructors.
          A.DotP PatInfo
r Expr
e -> do
            [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
r Expr
e) (DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
q') Dom Type
a]
            [NamedArg Pattern]
ps' <-
              case Expr -> AppView
appView Expr
e of
                -- If dot-pattern is an application of the constructor, try to preserve the
                -- arguments.
                Application (A.Con (A.AmbQ List1 QName
cs')) [NamedArg Expr]
es -> do
                  [ConHead]
cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a b. (a -> b) -> a -> b
$ List1 (Either SigError ConHead) -> [ConHead]
forall a b. List1 (Either a b) -> [b]
List1.rights (List1 (Either SigError ConHead) -> [ConHead])
-> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM QName -> TCM (Either SigError ConHead)
getConForm List1 QName
cs'
                  Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ConHead
c ConHead -> [ConHead] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ConHead]
cs') WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
                  [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ((NamedArg Expr -> NamedArg Pattern)
-> [NamedArg Expr] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg Expr -> NamedArg Pattern)
 -> [NamedArg Expr] -> [NamedArg Pattern])
-> ((Expr -> Pattern) -> NamedArg Expr -> NamedArg Pattern)
-> (Expr -> Pattern)
-> [NamedArg Expr]
-> [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Expr -> Named NamedName Pattern)
-> NamedArg Expr -> NamedArg Pattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName Expr -> Named NamedName Pattern)
 -> NamedArg Expr -> NamedArg Pattern)
-> ((Expr -> Pattern)
    -> Named NamedName Expr -> Named NamedName Pattern)
-> (Expr -> Pattern)
-> NamedArg Expr
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Pattern)
-> Named NamedName Expr -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
r) [NamedArg Expr]
es
                AppView
_  -> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          -- Andreas, 2016-12-29, issue #2363.
          -- Allow _ to stand for the corresponding parent pattern.
          A.WildP{} -> do
            -- Andreas, 2017-10-13, issue #2803:
            -- Delete the name, since it can confuse insertImplicitPattern.
            let ps' :: [NamedArg Pattern]
ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          -- Jesper, 2018-05-13, issue #2998.
          -- We also allow turning a constructor pattern into a variable.
          -- In general this is not type-safe since the types of some variables
          -- in the constructor pattern may have changed, so we have to
          -- re-check these solutions when checking the with clause (see LHS.hs)
          A.VarP BindName
x -> do
            [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP BindName
x) (DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
q') Dom Type
a]
            let ps' :: [NamedArg Pattern]
ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          A.ConP ConPatInfo
_ (A.AmbQ List1 QName
cs') [NamedArg Pattern]
ps' -> do
            -- Check whether the with-clause constructor can be (possibly trivially)
            -- disambiguated to be equal to the parent-clause constructor.
            -- Andreas, 2017-08-13, herein, ignore abstract constructors.
            [ConHead]
cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a b. (a -> b) -> a -> b
$ List1 (Either SigError ConHead) -> [ConHead]
forall a b. List1 (Either a b) -> [b]
List1.rights (List1 (Either SigError ConHead) -> [ConHead])
-> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM QName -> TCM (Either SigError ConHead)
getConForm List1 QName
cs'
            Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ConHead
c ConHead -> [ConHead] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ConHead]
cs') WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
            -- Strip the subpatterns ps' and then continue.
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          A.RecP KwRange
_ ConPatInfo
_ [FieldAssignment' Pattern]
fs -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe RecordData)
 -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData))
-> TCM (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
d) WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch ((RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \ RecordData
def -> do
            [NamedArg Pattern]
ps' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> Pattern)
-> [FieldAssignment' Pattern]
-> [Arg Name]
-> TCM [NamedArg Pattern]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (Pattern -> Name -> Pattern
forall a b. a -> b -> a
const (Pattern -> Name -> Pattern) -> Pattern -> Name -> Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) [FieldAssignment' Pattern]
fs
                                                 ((Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom Name]
recordFieldNames RecordData
def)
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConORec [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [NamedArg Pattern]
ps') -> do
             [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
               TCMT IO Doc
"stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
             WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

          Pattern
p -> do
           [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
             [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"with clause pattern is  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pattern -> [Char]
forall a. Show a => a -> [Char]
show Pattern
p
           WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch

        LitP PatternInfo
_ Literal
lit -> case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of
          A.LitP PatInfo
_ Literal
lit' | Literal
lit Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
lit' -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit
          A.WildP{}                   -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit

          p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [NamedArg Pattern
ps']) -> do
             [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
               TCMT IO Doc
"stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
             WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

          Pattern
_ -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
      where
        recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse Term
v = do
          let piOrPathApplyM :: Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v = do
                (TelV Telescope
tel Type
t', Boundary
bs) <- Int -> Type -> m (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary' Int
1 Type
t
                Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
                (Elims, Type) -> m (Elims, Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> Boundary -> Elims
forall a. DeBruijn a => Telescope -> Boundary' Int a -> [Elim' a]
teleElims Telescope
tel Boundary
bs, Int -> SubstArg Type -> Type -> Type
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg Type
v Type
t')
          (Elims
e, Type
t') <- Type -> Term -> WriterT [ProblemEq] (TCMT IO) (Elims, Type)
forall {m :: * -> *}. PureTCM m => Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v
          Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
e) Type
t' [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

        mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
        mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch = Telescope -> m a -> m a
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
delta (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$
          Pattern -> NamedArg DeBruijnPattern -> TypeError
WithClausePatternMismatch (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0) NamedArg DeBruijnPattern
q

        -- Make a WildP, keeping arg. info.
        makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern
        makeWildP :: NamedArg Pattern -> NamedArg Pattern
makeWildP = (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern)
-> (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern -> Pattern
forall a b. a -> b -> a
const (Pattern -> Pattern -> Pattern) -> Pattern -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange

        -- case I.ConP / A.ConP
        stripConP
          :: QName       -- Data type name of this constructor pattern.
          -> [Arg Term]  -- Data type arguments of this constructor pattern.
          -> Abs Type    -- Type the remaining patterns eliminate.
          -> ConHead     -- Constructor of this pattern.
          -> ConInfo     -- Constructor info of this pattern (constructor/record).
          -> [NamedArg DeBruijnPattern]  -- Argument patterns (parent clause).
          -> [NamedArg A.Pattern]        -- Argument patterns (with clause).
          -> WriterT [ProblemEq] TCM [NamedArg A.Pattern]  -- Stripped patterns.
        stripConP :: QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ci [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps' = do

          -- Get the type and number of parameters of the constructor.
          Defn {defType :: Definition -> Type
defType = Type
ct, theDef :: Definition -> Defn
theDef = Constructor{conPars :: Defn -> Int
conPars = Int
np}}  <- ConHead -> WriterT [ProblemEq] (TCMT IO) Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
          -- Compute the argument telescope for the constructor
          let ct' :: Type
ct' = Type
ct Type -> Args -> Type
`piApply` Int -> Args -> Args
forall a. Int -> [a] -> [a]
take Int
np Args
us
          TelV Telescope
tel' Type
_ <- TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type))
-> TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
ct'
          -- (TelV tel' _, _boundary) <- liftTCM $ telViewPathBoundary ct'

          [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
20 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
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
vcat [ TCMT IO Doc
"ct  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ct
                 , TCMT IO Doc
"ct' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ct'
                 , TCMT IO Doc
"np  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
np)
                 , 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((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
"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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((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 -> [TCMT IO Doc]) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Args
forall a. Int -> [a] -> [a]
take Int
np Args
us)
                 ]

          -- TODO Andrea: preserve IApplyP patterns in v, see _boundary?
          -- Compute the new type
          let v :: Term
v  = ConHead -> ConOrigin -> Elims -> Term
Con ConHead
c ConOrigin
ci [ Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Int -> Term
var Int
i) | (Int
i, Arg ArgInfo
info Named NamedName DeBruijnPattern
_) <- [Int]
-> [NamedArg DeBruijnPattern] -> [(Int, NamedArg DeBruijnPattern)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg DeBruijnPattern]
qs') [NamedArg DeBruijnPattern]
qs' ]
              t' :: Type
t' = Telescope
tel' Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
`abstract` Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp (Int -> Abs Type -> Abs Type
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Abs Type
b) Term
SubstArg Type
v
              self' :: Term
self' = Telescope
tel' Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
`abstract` Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Term
self) Term
v  -- Issue 1546

          [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
15 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
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
"inserting implicit"
            , 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
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, 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
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern]
ps' [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps)
            , 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
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t'
            ]

          -- Insert implicit patterns (just for the constructor arguments)
          [NamedArg Pattern]
psi' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps' Telescope
tel'
          Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([NamedArg Pattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg Pattern]
psi' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') (WriterT [ProblemEq] (TCMT IO) ()
 -> WriterT [ProblemEq] (TCMT IO) ())
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TypeError -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] (TCMT IO) ())
-> TypeError -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
            QName -> Int -> Int -> TypeError
WrongNumberOfConstructorArguments (ConHead -> QName
conName ConHead
c) (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') ([NamedArg Pattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg Pattern]
psi')

          -- Andreas, Ulf, 2016-06-01, Ulf's variant at issue #679
          -- Since instantiating the type with a constructor pattern
          -- can reveal more hidden arguments, we need to insert them here.
          [NamedArg Pattern]
psi <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast ([NamedArg Pattern]
psi' [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps) Type
t'

          -- Keep going
          Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self' Type
t' [NamedArg Pattern]
psi ([NamedArg DeBruijnPattern]
qs' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
qs)

-- | Construct the display form for a with function. It will display
--   applications of the with function as applications to the original function.
--   For instance,
--
--   @
--     aux a b c
--   @
--
--   as
--
--   @
--     f (suc a) (suc b) | c
--   @
withDisplayForm
  :: QName
       -- ^ The name of parent function.
  -> QName
       -- ^ The name of the @with@-function.
  -> Telescope
       -- ^ __@Δ₁@__     The arguments of the @with@ function before the @with@ expressions.
  -> Telescope
       -- ^ __@Δ₂@__     The arguments of the @with@ function after the @with@ expressions.
  -> Nat
       -- ^ __@n@__      The number of @with@ expressions.
  -> [NamedArg DeBruijnPattern]
      -- ^ __@qs@__      The parent patterns.
  -> Permutation
      -- ^ __@perm@__    Permutation to split into needed and unneeded vars.
  -> Permutation
      -- ^ __@lhsPerm@__ Permutation reordering the variables in parent patterns.
  -> TCM DisplayForm
withDisplayForm :: QName
-> QName
-> Telescope
-> Telescope
-> Int
-> [NamedArg DeBruijnPattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm QName
f QName
aux Telescope
delta1 Telescope
delta2 Int
n [NamedArg DeBruijnPattern]
qs perm :: Permutation
perm@(Perm Int
m [Int]
_) Permutation
lhsPerm = do

  -- Compute the arity of the display form.
  let arity0 :: Int
arity0 = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
  -- The currently free variables have to be added to the front.
  Args
topArgs <- Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise Int
arity0 (Args -> Args) -> TCMT IO Args -> TCMT IO Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  let top :: Int
top    = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
topArgs
      arity :: Int
arity  = Int
arity0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top

  -- Build the rhs of the display form.
  Term
wild <- TCMT IO Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_ TCMT IO Name -> (Name -> Term) -> TCM Term
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Name
x -> QName -> Elims -> Term
Def (Name -> QName
qualify_ Name
x) []
  let -- Convert the parent patterns to terms.
      tqs0 :: [Elim' DisplayTerm]
tqs0       = [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
patsToElims [NamedArg DeBruijnPattern]
qs
      -- Build a substitution to replace the parent pattern vars
      -- by the pattern vars of the with-function.
      ([Int]
ys0, [Int]
ys1) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta1) ([Int] -> ([Int], [Int])) -> [Int] -> ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ Permutation -> [Int] -> [Int]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
m
      ys :: [Maybe Int]
ys         = [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a]
reverse ((Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys0 [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ Int -> Maybe Int -> [Maybe Int]
forall a. Int -> a -> [a]
replicate Int
n Maybe Int
forall a. Maybe a
Nothing [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys1)
                   [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+)) [Int
0..Int
topInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
      rho :: Substitution' Term
rho        = Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild
      tqs :: [Elim' DisplayTerm]
tqs        = Substitution' (SubstArg [Elim' DisplayTerm])
-> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Elim' DisplayTerm])
rho [Elim' DisplayTerm]
tqs0
      -- Build the arguments to the with function.
      es :: [Elim' DisplayTerm]
es         = (Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
topArgs [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ [Elim' DisplayTerm]
tqs
      withArgs :: NonEmpty Term
withArgs   = NonEmpty Term -> [Term] -> NonEmpty Term
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe NonEmpty Term
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Term] -> NonEmpty Term) -> [Term] -> NonEmpty Term
forall a b. (a -> b) -> a -> b
$  -- List is non-empty since n >= 1
                     (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ 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
delta2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
      dt :: DisplayTerm
dt         = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp (QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
f [Elim' DisplayTerm]
es) ((Term -> DisplayTerm) -> NonEmpty Term -> List1 DisplayTerm
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm NonEmpty Term
withArgs) []

  -- Build the lhs of the display form and finish.
  -- @var 0@ is the pattern variable (hole).
  let display :: DisplayForm
display = Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
arity [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i | Int
i <- Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
arity] DisplayTerm
dt

  -- Debug printing.
  let addFullCtx :: TCMT IO Doc -> TCMT IO Doc
addFullCtx = 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
delta1
                 (TCMT IO Doc -> TCMT IO Doc)
-> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCMT IO Doc -> [[Char]] -> TCMT IO Doc)
-> [[Char]] -> TCMT IO Doc -> TCMT IO Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip (([Char] -> TCMT IO Doc -> TCMT IO Doc)
-> TCMT IO Doc -> [[Char]] -> TCMT IO Doc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Char] -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
addContext) ([Int] -> (Int -> [Char]) -> [[Char]]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
for [Int
1..Int
n] ((Int -> [Char]) -> [[Char]]) -> (Int -> [Char]) -> [[Char]]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> [Char]
"w" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)
                 (TCMT IO Doc -> TCMT IO Doc)
-> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
delta2
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.display" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
vcat
    [ TCMT IO Doc
"withDisplayForm"
    , 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
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"f      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f)
      , TCMT IO Doc
"aux    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
aux)
      , TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta1
      , TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do 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
delta1 (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
delta2
      , TCMT IO Doc
"n      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
      , TCMT IO Doc
"perm   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
      , TCMT IO Doc
"top    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
topArgs
      , TCMT IO Doc
"qs     =" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
qs)
      , TCMT IO Doc
"qsToTm =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim' DisplayTerm] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim' DisplayTerm] -> m Doc
prettyTCM [Elim' DisplayTerm]
tqs0 -- ctx would be permuted form of delta1 ++ delta2
      , TCMT IO Doc
"ys     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Maybe Int] -> [Char]
forall a. Show a => a -> [Char]
show [Maybe Int]
ys)
      , TCMT IO Doc
"rho    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Substitution' Term -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Substitution' Term
rho)
      , TCMT IO Doc
"qs[rho]=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Elim' DisplayTerm] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim' DisplayTerm] -> m Doc
prettyTCM [Elim' DisplayTerm]
tqs
      , TCMT IO Doc
"dt     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ DisplayTerm -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM DisplayTerm
dt
      ]
    ]
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.display" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"raw    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (DisplayForm -> [Char]
forall a. Show a => a -> [Char]
show DisplayForm
display)
      ]

  DisplayForm -> TCM DisplayForm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return DisplayForm
display
  where
    -- Ulf, 2014-02-19: We need to rename the module parameters as well! (issue1035)
    -- sub top ys wild = map term [0 .. m - 1] ++# raiseS (length qs)
    -- Andreas, 2015-10-28: Yes, but properly! (Issue 1407)
    sub :: Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
term [Int
0 .. Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
      where
        term :: Int -> Term
term Int
i = Term -> (Int -> Term) -> Maybe Int -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
wild Int -> Term
var (Maybe Int -> Term) -> Maybe Int -> Term
forall a b. (a -> b) -> a -> b
$ Maybe Int -> [Maybe Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) [Maybe Int]
ys

-- Andreas, 2014-12-05 refactored using numberPatVars
-- Andreas, 2013-02-28 modeled after Coverage/Match/buildMPatterns
patsToElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
patsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
patsToElims = (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Elim' DisplayTerm)
 -> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm])
-> (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
-> [NamedArg DeBruijnPattern]
-> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ Arg DeBruijnPattern -> Elim' DisplayTerm
toElim (Arg DeBruijnPattern -> Elim' DisplayTerm)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing
  where
    toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm
    toElim :: Arg DeBruijnPattern -> Elim' DisplayTerm
toElim (Arg ArgInfo
ai DeBruijnPattern
p) = case DeBruijnPattern
p of
      ProjP ProjOrigin
o QName
d -> ProjOrigin -> QName -> Elim' DisplayTerm
forall a. ProjOrigin -> QName -> Elim' a
I.Proj ProjOrigin
o QName
d
      DeBruijnPattern
p         -> Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> Arg DisplayTerm -> Elim' DisplayTerm
forall a b. (a -> b) -> a -> b
$ ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p

    toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
    toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms = (NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Arg DisplayTerm)
 -> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm])
-> (NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> [NamedArg DeBruijnPattern]
-> [Arg DisplayTerm]
forall a b. (a -> b) -> a -> b
$ (Named NamedName DeBruijnPattern -> DisplayTerm)
-> NamedArg DeBruijnPattern -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName DeBruijnPattern -> DisplayTerm)
 -> NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> (Named NamedName DeBruijnPattern -> DisplayTerm)
-> NamedArg DeBruijnPattern
-> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> DisplayTerm
toTerm (DeBruijnPattern -> DisplayTerm)
-> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> Named NamedName DeBruijnPattern
-> DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing

    toTerm :: DeBruijnPattern -> DisplayTerm
    toTerm :: DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p = case PatternInfo -> PatOrigin
patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Maybe PatternInfo -> PatternInfo
forall a. a -> Maybe a -> a
fromMaybe PatternInfo
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe PatternInfo -> PatternInfo)
-> Maybe PatternInfo -> PatternInfo
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p of
      PatOrigin
PatOSystem -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatOSplit  -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOSplitArg{} -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
      PatOVar{}  -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
      PatOrigin
PatODot    -> Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p
      PatOrigin
PatOWild   -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
      PatOrigin
PatOCon    -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatORec    -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatOLit    -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatOAbsurd -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p -- see test/Succeed/Issue2849.agda

    toDisplayPattern :: DeBruijnPattern -> DisplayTerm
    toDisplayPattern :: DeBruijnPattern -> DisplayTerm
toDisplayPattern = \case
      IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x -- TODO, should be an Elim' DisplayTerm ?
      ProjP ProjOrigin
_ QName
d  -> DisplayTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
      VarP PatternInfo
i DBPatVar
x -> Term -> DisplayTerm
DTerm  (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
      DotP PatternInfo
i Term
t -> Term -> DisplayTerm
DDot   (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term
t
      p :: DeBruijnPattern
p@(ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps) -> ConHead -> ConOrigin -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c (ConPatternInfo -> ConOrigin
fromConPatternInfo ConPatternInfo
cpi) ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms [NamedArg DeBruijnPattern]
ps
      LitP PatternInfo
i Literal
l -> Term -> DisplayTerm
DTerm  (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
      DefP PatternInfo
_ QName
q [NamedArg DeBruijnPattern]
ps -> QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
q ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ (Arg DisplayTerm -> Elim' DisplayTerm)
-> [Arg DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply ([Arg DisplayTerm] -> [Elim' DisplayTerm])
-> [Arg DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms [NamedArg DeBruijnPattern]
ps

    toVarOrDot :: DeBruijnPattern -> DisplayTerm
    toVarOrDot :: DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p = case DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p of
      Var Int
i [] -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
      Term
t        -> Term -> DisplayTerm
DDot Term
t