{-# 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 :: Tele (Dom Type)
-> Type
-> NonEmpty (Arg (Term, EqualityView))
-> (Tele (Dom Type), Tele (Dom Type), Permutation, Type,
    NonEmpty (Arg (Term, EqualityView)))
splitTelForWith Tele (Dom Type)
delta Type
t NonEmpty (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 = NonEmpty (Arg (Term, EqualityView)) -> VarSet
forall t. Free t => t -> VarSet
freeVarSet NonEmpty (Arg (Term, EqualityView))
vtys
    SplitTel Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 Permutation
perm = VarSet -> Tele (Dom Type) -> SplitTel
splitTelescope VarSet
fv Tele (Dom Type)
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
$ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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' :: NonEmpty (Arg (Term, EqualityView))
vtys' = Substitution' (SubstArg (NonEmpty (Arg (Term, EqualityView))))
-> NonEmpty (Arg (Term, EqualityView))
-> NonEmpty (Arg (Term, EqualityView))
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (NonEmpty (Arg (Term, EqualityView))))
rhopi NonEmpty (Arg (Term, EqualityView))
vtys

  in (Tele (Dom Type)
delta1, Tele (Dom Type)
delta2, Permutation
perm, Type
t', NonEmpty (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 :: Tele (Dom Type)
-> NonEmpty (Arg (Term, EqualityView))
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCM (Type, (Int, Int))
withFunctionType Tele (Dom Type)
delta1 NonEmpty (Arg (Term, EqualityView))
vtys Tele (Dom Type)
delta2 Type
b Boundary
bndry = Tele (Dom Type) -> 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 =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
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

  d2b <- Tele (Dom Type) -> Type -> Boundary -> TCM Type
telePiPath_ Tele (Dom Type)
delta2 Type
b Boundary
bndry
  dbg 30 "Δ₂ → B" d2b
  d2b  <- normalise d2b
  dbg 30 "normal Δ₂ → B" d2b
  d2b  <- etaContract d2b
  dbg 30 "eta-contracted Δ₂ → B" d2b

  vtys <- etaContract =<< normalise vtys

  -- wd2b = wtel → [vs : as] (Δ₂ → B)
  wd2b <- foldrM piAbstract d2b vtys
  dbg 30 "wΓ → Δ₂ → B" wd2b

  let 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)
-> NonEmpty (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) NonEmpty (Arg (Term, EqualityView))
vtys
  let nwithpats = NonEmpty (Arg (Term, EqualityView)) -> Int
forall (f :: * -> *).
(Functor f, Foldable f) =>
f (Arg (Term, EqualityView)) -> Int
countWithPats NonEmpty (Arg (Term, EqualityView))
vtys

  TelV wtel _ <- telViewUpTo nwithargs wd2b

  -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂"
  let 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 = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta2
              lams :: Term -> Term
lams = Tele (Dom Type) -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs Tele (Dom Type)
wtel (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
delta2

  d1wd2b <- telePiPath_ delta1 wd2b bndry'

  dbg 30 "Δ₁ → wΓ → Δ₂ → B" d1wd2b

  return (d1wd2b, (nwithargs, 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 :: NonEmpty (Arg (Term, EqualityView)) -> TCM (NonEmpty (Arg Term))
withArguments NonEmpty (Arg (Term, EqualityView))
vtys = do
  NonEmpty (NonEmpty (Arg Term)) -> NonEmpty (Arg Term)
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (NonEmpty (Arg Term)) -> NonEmpty (Arg Term))
-> TCMT IO (NonEmpty (NonEmpty (Arg Term)))
-> TCM (NonEmpty (Arg Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    NonEmpty (Arg (Term, EqualityView))
-> (Arg (Term, EqualityView) -> TCM (NonEmpty (Arg Term)))
-> TCMT IO (NonEmpty (NonEmpty (Arg Term)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty (Arg (Term, EqualityView))
vtys ((Arg (Term, EqualityView) -> TCM (NonEmpty (Arg Term)))
 -> TCMT IO (NonEmpty (NonEmpty (Arg Term))))
-> (Arg (Term, EqualityView) -> TCM (NonEmpty (Arg Term)))
-> TCMT IO (NonEmpty (NonEmpty (Arg Term)))
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info (Term, EqualityView)
ts) -> do
      (Term -> Arg Term) -> NonEmpty Term -> NonEmpty (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 -> NonEmpty (Arg Term))
-> TCMT IO (NonEmpty Term) -> TCM (NonEmpty (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' SrcFile
_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
            mkRefl <- TCM (Arg Term -> Term)
getRefl
            return $ v :| mkRefl (defaultArg v) : []

-- | 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
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> Int
-> Substitution' Term
-> Permutation
-> Int
-> Int
-> List1 (Clause' SpineLHS)
-> TCM (List1 (Clause' SpineLHS))
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Tele (Dom Type)
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
_ [Arg (Named_ Pattern)]
allPs) [ProblemEq]
inheritedPats RHS
rhs WhereDeclarations
wh Catchall
catchall) = do
      let ([Arg (Named_ Pattern)]
ps, [Arg (Named_ Pattern)]
wps)    = [Arg (Named_ Pattern)]
-> ([Arg (Named_ Pattern)], [Arg (Named_ Pattern)])
splitOffTrailingWithPatterns [Arg (Named_ Pattern)]
allPs
          ([Arg (Named_ Pattern)]
wps0, [Arg (Named_ Pattern)]
wps1) = Int
-> [Arg (Named_ Pattern)]
-> ([Arg (Named_ Pattern)], [Arg (Named_ Pattern)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Named_ Pattern)]
wps
          ps0 :: [Arg (Named_ Pattern)]
ps0          = (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> Pattern
forall {e}. Pattern' e -> Pattern' e
fromWithP) [Arg (Named_ 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
<+> [Arg (Named_ Pattern)] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Arg (Named_ 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
<+> [Arg (Named_ Pattern)] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Arg (Named_ 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
<+> [Arg (Named_ Pattern)] -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Arg (Named_ 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 ([Arg (Named_ Pattern)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg (Named_ 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
        ]
      (strippedPats, ps') <- [Name]
-> QName
-> QName
-> Type
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [Arg (Named_ Pattern)]
-> TCM ([ProblemEq], [Arg (Named_ Pattern)])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [Arg (Named_ Pattern)]
ps
      reportSDoc "tc.with" 50 $ hang "strippedPats:" 2 $
                                  vcat [ prettyA p <+> "==" <+> prettyTCM v <+> (":" <+> prettyTCM t)
                                       | A.ProblemEq p v t <- strippedPats ]
      rhs <- buildRHS strippedPats rhs
      let (ps1, ps2) = splitAt n1 ps'
      let result = SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
A.Clause (LHSInfo -> QName -> [Arg (Named_ Pattern)] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux ([Arg (Named_ Pattern)] -> SpineLHS)
-> [Arg (Named_ Pattern)] -> SpineLHS
forall a b. (a -> b) -> a -> b
$ [Arg (Named_ Pattern)]
ps1 [Arg (Named_ Pattern)]
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern)]
ps0 [Arg (Named_ Pattern)]
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern)]
ps2 [Arg (Named_ Pattern)]
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern)]
wps1)
                     ([ProblemEq]
inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
                     RHS
rhs WhereDeclarations
wh Catchall
catchall
      reportSDoc "tc.with" 20 $ vcat
        [ "buildWithClause returns" <+> prettyA result
        ]
      return 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' LHS)
cs)         = QName -> List1 WithExpr -> List1 (Clause' LHS) -> RHS
A.WithRHS QName
q List1 WithExpr
es (List1 (Clause' LHS) -> RHS)
-> TCMT IO (List1 (Clause' LHS)) -> TCMT IO RHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      (Clause' LHS -> TCMT IO (Clause' LHS))
-> List1 (Clause' LHS) -> TCMT IO (List1 (Clause' LHS))
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' LHS
forall a b. LHSToSpine a b => b -> a
A.spineToLhs (Clause' SpineLHS -> Clause' LHS)
-> (Clause' SpineLHS -> Clause' SpineLHS)
-> Clause' SpineLHS
-> Clause' LHS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots) (Clause' SpineLHS -> Clause' LHS)
-> (Clause' LHS -> TCMT IO (Clause' SpineLHS))
-> Clause' LHS
-> TCMT IO (Clause' LHS)
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' LHS -> Clause' SpineLHS)
-> Clause' LHS
-> TCMT IO (Clause' SpineLHS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' LHS -> Clause' SpineLHS
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine) List1 (Clause' LHS)
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
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [Arg (Named_ Pattern)]
-> TCM ([ProblemEq], [Arg (Named_ Pattern)])
stripWithClausePatterns [Name]
cxtNames QName
parent QName
f Type
t Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [Arg (Named_ Pattern)]
ps = do
  -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074)
  ps <- [Arg (Named_ Pattern)] -> TCM [Arg (Named_ Pattern)]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [Arg (Named_ 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
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' = (Int -> NamedArg DeBruijnPattern -> Arg (Named_ Pattern))
-> [Int] -> [NamedArg DeBruijnPattern] -> [Arg (Named_ Pattern)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((Named NamedName DeBruijnPattern -> Named_ Pattern)
-> NamedArg DeBruijnPattern -> Arg (Named_ 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_ Pattern)
 -> NamedArg DeBruijnPattern -> Arg (Named_ Pattern))
-> (Int -> Named NamedName DeBruijnPattern -> Named_ Pattern)
-> Int
-> NamedArg DeBruijnPattern
-> Arg (Named_ Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> Pattern)
-> Named NamedName DeBruijnPattern -> Named_ 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_ Pattern)
-> (Int -> DeBruijnPattern -> Pattern)
-> Int
-> Named NamedName DeBruijnPattern
-> Named_ 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) [Arg (Named_ Pattern)]
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern)]
ps
  psi <- insertImplicitPatternsT ExpandLast ps' t
  reportSDoc "tc.with.strip" 10 $ vcat
    [ "stripping patterns"
    , nest 2 $ "t   = " <+> prettyTCM t
    , nest 2 $ "ps  = " <+> fsep (punctuate comma $ map prettyA ps)
    , nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
    , nest 2 $ "psi = " <+> fsep (punctuate comma $ map prettyA psi)
    , nest 2 $ addContext delta $
               "qs  = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
    , nest 2 $ "perm= " <+> text (show perm)
    ]

  -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function!
  (ps', strippedPats) <- runWriterT $ addContext delta $
    strip (Def parent []) t psi qs
  unless (null strippedPats) $ reportSDoc "tc.with.strip" 50 $ nest 2 $
    "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
  let psp = Permutation -> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [Arg (Named_ Pattern)]
ps'
  reportSDoc "tc.with.strip" 10 $ vcat
    [ nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
    , nest 2 $ "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
    ]
  return (strippedPats, 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
$ Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
delta

    setVarArgInfo :: DBPatVar -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
setVarArgInfo DBPatVar
x Arg (Named_ Pattern)
p = Origin -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a. LensOrigin a => Origin -> a -> a
setOrigin (Arg (Named_ Pattern) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ Pattern)
p) (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (DBPatVar -> ArgInfo
varArgInfo DBPatVar
x) Arg (Named_ 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
-> [Arg (Named_ Pattern)]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ 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.
      ps <- TCM [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [Arg (Named_ Pattern)]
 -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> TCM [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [Arg (Named_ Pattern)] -> Type -> TCM [Arg (Named_ Pattern)]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [Arg (Named_ Pattern)] -> Type -> m [Arg (Named_ Pattern)]
insertImplicitPatternsT ExpandHidden
ExpandLast [] Type
t
      if null ps then typeError TooFewPatternsInWithClause
       else strip self t ps 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
_ [Arg (Named_ 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 ((Arg (Named_ Pattern) -> Bool) -> [Arg (Named_ Pattern)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern -> Bool
forall {e}. Pattern' e -> Bool
implicit (Pattern -> Bool)
-> (Arg (Named_ Pattern) -> Pattern)
-> Arg (Named_ Pattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg) [Arg (Named_ 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
      [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ 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 (Arg (Named_ Pattern)
p0 : [Arg (Named_ Pattern)]
ps) qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
_)
      | A.AsP PatInfo
_ BindName
x Pattern
p <- Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
p0 = do
        (a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
        let v = DeBruijnPattern -> Term
patternToTerm (NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
q)
        tell [ProblemEq (A.VarP x) v a]
        strip self t (fmap (p <$) p0 : ps) qs
    strip Term
self Type
t ps0 :: [Arg (Named_ Pattern)]
ps0@(Arg (Named_ Pattern)
p0 : [Arg (Named_ Pattern)]
ps) qs0 :: [NamedArg DeBruijnPattern]
qs0@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
qs) = do
      p <- ((Named_ Pattern -> WriterT [ProblemEq] (TCMT IO) (Named_ Pattern))
-> Arg (Named_ Pattern)
-> WriterT [ProblemEq] (TCMT IO) (Arg (Named_ 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_ Pattern -> WriterT [ProblemEq] (TCMT IO) (Named_ Pattern))
 -> Arg (Named_ Pattern)
 -> WriterT [ProblemEq] (TCMT IO) (Arg (Named_ Pattern)))
-> ((Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
    -> Named_ Pattern
    -> WriterT [ProblemEq] (TCMT IO) (Named_ Pattern))
-> (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
-> Arg (Named_ Pattern)
-> WriterT [ProblemEq] (TCMT IO) (Arg (Named_ Pattern))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
-> Named_ Pattern -> WriterT [ProblemEq] (TCMT IO) (Named_ 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 Arg (Named_ Pattern)
p0
      reportSDoc "tc.with.strip" 15 $ vcat
        [ "strip"
        , nest 2 $ "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0)
        , nest 2 $ "exp =" <+> prettyA p
        , nest 2 $ "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0)
        , nest 2 $ "self=" <+> prettyTCM self
        , nest 2 $ "t   =" <+> prettyTCM t
        ]
      case namedArg q of
        ProjP ProjOrigin
o QName
d -> case Arg (Named_ Pattern) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP Arg (Named_ Pattern)
p of
          Just (ProjOrigin
o', AmbiguousQName
ambP) -> 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
$ Arg (Named_ Pattern)
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Arg (Named_ 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
$ 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]
++ Arg (Named_ Pattern) -> [Char]
forall a. Show a => a -> [Char]
show Arg (Named_ 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' SrcFile -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Arg (Named_ Pattern) -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Arg (Named_ 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
$ Arg (Named_ Pattern)
-> ProjOrigin -> NamedArg DeBruijnPattern -> ProjOrigin -> Warning
WithClauseProjectionFixityMismatch Arg (Named_ 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.
            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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m QName
getOriginalProjection QName
d
            found <- existsM (getAmbiguous ambP) $ \ 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 not found then mismatch else do
              (self1, t1, ps) <- liftTCM $ do
                t <- reduce t
                (_, self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t o 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.
                ps <- insertImplicitPatternsT ExpandLast ps t1
                return (self1, t1, ps)
              strip self1 t1 ps qs
          Maybe (ProjOrigin, AmbiguousQName)
Nothing -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (m :: * -> *) a. 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 <- Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
p
                 , A.Var Name
y <- Expr -> Expr
unScope Expr
u -> do
          (DBPatVar -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
setVarArgInfo DBPatVar
x (Arg (Named_ Pattern) -> Pattern -> Arg (Named_ Pattern)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg Arg (Named_ Pattern)
p (Pattern -> Arg (Named_ Pattern))
-> Pattern -> Arg (Named_ 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) Arg (Named_ Pattern)
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. a -> [a] -> [a]
:) ([Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)])
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))

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

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

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

        DotP PatternInfo
i Term
v  -> do
          (a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
          tell [ProblemEq (namedArg p) v a]
          case v of
            Var Int
x [] | PatOVar{} <- PatternInfo -> PatOrigin
patOrigin PatternInfo
i
               -> (Arg (Named_ Pattern)
p Arg (Named_ Pattern)
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. a -> [a] -> [a]
:) ([Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)])
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
recurse (Int -> Term
var Int
x)
            Term
_  -> (Arg (Named_ Pattern) -> Arg (Named_ Pattern)
makeWildP Arg (Named_ Pattern)
p Arg (Named_ Pattern)
-> [Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)]
forall a. a -> [a] -> [a]
:) ([Arg (Named_ Pattern)] -> [Arg (Named_ Pattern)])
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ 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
         (a, 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 d es <- liftTCM $ reduce (unEl $ unDom a)
         let us = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
         -- Get the original constructor and field names.
         c <- either __IMPOSSIBLE__ (`withRangeOf` c) <$> do liftTCM $ getConForm $ conName c

         case namedArg 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]
            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 AmbiguousQName
cs') [NamedArg Expr]
es -> do
                  WriterT [ProblemEq] (TCMT IO) Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (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
$ ConHead
c ConHead -> AmbiguousQName -> TCM Bool
`elemConForms` AmbiguousQName
cs') WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a. MonadTCError m => m a
mismatch
                  [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg (Named_ Pattern)]
 -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ ((NamedArg Expr -> Arg (Named_ Pattern))
-> [NamedArg Expr] -> [Arg (Named_ Pattern)]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg Expr -> Arg (Named_ Pattern))
 -> [NamedArg Expr] -> [Arg (Named_ Pattern)])
-> ((Expr -> Pattern) -> NamedArg Expr -> Arg (Named_ Pattern))
-> (Expr -> Pattern)
-> [NamedArg Expr]
-> [Arg (Named_ Pattern)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Expr -> Named_ Pattern)
-> NamedArg Expr -> Arg (Named_ 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_ Pattern)
 -> NamedArg Expr -> Arg (Named_ Pattern))
-> ((Expr -> Pattern) -> Named NamedName Expr -> Named_ Pattern)
-> (Expr -> Pattern)
-> NamedArg Expr
-> Arg (Named_ Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Pattern) -> Named NamedName Expr -> Named_ 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
_  -> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg (Named_ Pattern)]
 -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> Arg (Named_ Pattern))
-> [NamedArg DeBruijnPattern] -> [Arg (Named_ Pattern)]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named_ 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_ Pattern -> NamedArg DeBruijnPattern -> Arg (Named_ Pattern)
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            stripConP d us b c ConOCon qs' 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' :: [Arg (Named_ Pattern)]
ps' = (NamedArg DeBruijnPattern -> Arg (Named_ Pattern))
-> [NamedArg DeBruijnPattern] -> [Arg (Named_ Pattern)]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named_ 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_ Pattern -> NamedArg DeBruijnPattern -> Arg (Named_ 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]
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [Arg (Named_ 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' :: [Arg (Named_ Pattern)]
ps' = (NamedArg DeBruijnPattern -> Arg (Named_ Pattern))
-> [NamedArg DeBruijnPattern] -> [Arg (Named_ Pattern)]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named_ 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_ Pattern -> NamedArg DeBruijnPattern -> Arg (Named_ 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]
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [Arg (Named_ Pattern)]
ps'

          A.ConP ConPatInfo
_ AmbiguousQName
ambC [Arg (Named_ 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.
            WriterT [ProblemEq] (TCMT IO) Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (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
$ ConHead
c ConHead -> AmbiguousQName -> TCM Bool
`elemConForms` AmbiguousQName
ambC) WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a. MonadTCError m => m a
mismatch
            -- Strip the subpatterns ps' and then continue.
            QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [Arg (Named_ Pattern)]
ps'

          A.RecP KwRange
_ ConPatInfo
_ [FieldAssignment' Pattern]
fs -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
-> (RecordData
    -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ 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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
d) WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (m :: * -> *) a. MonadTCError m => m a
mismatch ((RecordData
  -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
 -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> (RecordData
    -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ \ RecordData
def -> do
            ps' <- TCM [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [Arg (Named_ Pattern)]
 -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> TCM [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ ConOrigin
-> QName
-> (Name -> Pattern)
-> [FieldAssignment' Pattern]
-> [Arg Name]
-> TCM [Arg (Named_ Pattern)]
forall a.
HasRange a =>
ConOrigin
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail ConOrigin
ConORec 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)
            stripConP d us b c ConORec qs' ps'

          p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [Arg (Named_ 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) [Arg (Named_ 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) [Arg (Named_ Pattern)]
forall (m :: * -> *) a. MonadTCError m => m a
mismatch

        LitP PatternInfo
_ Literal
lit -> case Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ 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) [Arg (Named_ Pattern)]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit
          A.WildP{}                   -> Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)])
-> Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit

          p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [Arg (Named_ 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) [Arg (Named_ Pattern)]
forall a. HasCallStack => a
__IMPOSSIBLE__

          Pattern
_ -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
forall (m :: * -> *) a. MonadTCError m => m a
mismatch
      where
        recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
recurse Term
v = do
          let piOrPathApplyM :: Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v = do
                (TelV tel t', bs) <- Int -> Type -> m (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary' Int
1 Type
t
                unless (size tel == 1) $ __IMPOSSIBLE__
                return (teleElims tel bs, subst 0 v t')
          (e, t') <- Type -> Term -> WriterT [ProblemEq] (TCMT IO) (Elims, Type)
forall {m :: * -> *}. PureTCM m => Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v
          strip (self `applyE` e) t' ps qs

        mismatch :: forall m a. MonadTCError m => m a
        mismatch :: forall (m :: * -> *) a. MonadTCError m => m a
mismatch = 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 (Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
p0) NamedArg DeBruijnPattern
q

        -- Make a WildP, keeping arg. info.
        makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern
        makeWildP :: Arg (Named_ Pattern) -> Arg (Named_ Pattern)
makeWildP = (Pattern -> Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Pattern -> Pattern)
 -> Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> (Pattern -> Pattern)
-> Arg (Named_ Pattern)
-> Arg (Named_ 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]
-> [Arg (Named_ Pattern)]
-> WriterT [ProblemEq] (TCMT IO) [Arg (Named_ Pattern)]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ci [NamedArg DeBruijnPattern]
qs' [Arg (Named_ Pattern)]
ps' = do

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

          reportSDoc "tc.with.strip" 20 $
            vcat [ "ct  = " <+> prettyTCM ct
                 , "ct' = " <+> prettyTCM ct'
                 , "np  = " <+> text (show np)
                 , "us  = " <+> prettyList (map prettyTCM us)
                 , "us' = " <+> prettyList (map prettyTCM $ take np us)
                 ]

          -- TODO Andrea: preserve IApplyP patterns in v, see _boundary?
          -- Compute the new type
          let 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' = Tele (Dom Type)
tel' Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> 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 (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel') Abs Type
b) Term
SubstArg Type
v
              self' = Tele (Dom Type)
tel' Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> 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 (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel') Term
self) Term
v  -- Issue 1546

          reportSDoc "tc.with.strip" 15 $ sep
            [ "inserting implicit"
            , nest 2 $ prettyList $ map prettyA (ps' ++ ps)
            , nest 2 $ ":" <+> prettyTCM t'
            ]

          -- Insert implicit patterns (just for the constructor arguments)
          psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel'
          unless (size psi' == size tel') $ typeError $
            WrongNumberOfConstructorArguments (conName c) (size tel') (size 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.
          psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t'

          -- Keep going
          strip self' t' psi (qs' ++ qs)

-- | Is the first name equal to the 'constructorForm' of any disambiguation of the second name?
elemConForms :: ConHead -> AmbiguousQName -> TCM Bool
elemConForms :: ConHead -> AmbiguousQName -> TCM Bool
elemConForms ConHead
c AmbiguousQName
cs =
  NonEmpty QName -> (QName -> TCM Bool) -> TCM Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
existsM (AmbiguousQName -> NonEmpty QName
getAmbiguous AmbiguousQName
cs) \ QName
c' ->
    HasCallStack => QName -> TCM (Either SigError ConHead)
QName -> TCM (Either SigError ConHead)
getConForm QName
c' TCM (Either SigError ConHead)
-> (Either SigError ConHead -> Bool) -> TCM Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Left{}   -> Bool
False
      Right ConHead
c' -> ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c'

-- | 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
-> Tele (Dom Type)
-> Tele (Dom Type)
-> Int
-> [NamedArg DeBruijnPattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm QName
f QName
aux Tele (Dom Type)
delta1 Tele (Dom Type)
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
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta2
  -- The currently free variables have to be added to the front.
  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    = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
topArgs
      arity  = Int
arity0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top

  -- Build the rhs of the display form.
  wild <- freshNoName_ <&> \ Name
x -> QName -> Elims -> Term
Def (Name -> QName
qualify_ Name
x) []
  let -- Convert the parent patterns to terms.
      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.
      (ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m
      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        = Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild
      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         = (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 -> [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
$ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
      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 = 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 = Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
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
. Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta2
  reportSDoc "tc.with.display" 20 $ vcat
    [ "withDisplayForm"
    , nest 2 $ vcat
      [ "f      =" <+> text (prettyShow f)
      , "aux    =" <+> text (prettyShow aux)
      , "delta1 =" <+> prettyTCM delta1
      , "delta2 =" <+> do addContext delta1 $ prettyTCM delta2
      , "n      =" <+> text (show n)
      , "perm   =" <+> text (show perm)
      , "top    =" <+> do addFullCtx $ prettyTCM topArgs
      , "qs     =" <+> prettyList (map pretty qs)
      , "qsToTm =" <+> prettyTCM tqs0 -- ctx would be permuted form of delta1 ++ delta2
      , "ys     =" <+> text (show ys)
      , "rho    =" <+> text (prettyShow rho)
      , "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs
      , "dt     =" <+> do addFullCtx $ prettyTCM dt
      ]
    ]
  reportSDoc "tc.with.display" 70 $ nest 2 $ vcat
      [ "raw    =" <+> text (show display)
      ]

  return 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