{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.With where

import Prelude hiding ((!!))

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

import Data.Either
import qualified Data.List as List
import Data.Maybe
import Data.Foldable ( foldrM )

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.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive ( getRefl )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path

import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..))

import Agda.Utils.Functor
import Agda.Utils.List
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.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
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.
  -> [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 @π@
     , [Arg (Term, EqualityView)]        -- @Δ₁ ⊢ vs' : as'@ with- and rewrite-arguments and types under @π@.
     )              -- ^ (__@Δ₁@__,__@Δ₂@__,__@π@__,__@t'@__,__@vtys'@__) where
--
--   [@Δ₁@]        part of context needed for with arguments and their types.
--
--   [@Δ₂@]        part of context not needed for with arguments and their types.
--
--   [@π@]         permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
--
--   [@Δ₁Δ₂ ⊢ t'@] type of rhs under @π@
--
--   [@Δ₁ ⊢ vtys'@]  with-arguments and their types under @π@.

splitTelForWith :: Telescope
-> Type
-> [Arg (Term, EqualityView)]
-> (Telescope, Telescope, Permutation, Type,
    [Arg (Term, EqualityView)])
splitTelForWith Telescope
delta Type
t [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 = forall t. Free t => t -> VarSet
allFreeVars [Arg (Term, EqualityView)]
vtys
    SplitTel Telescope
delta1 Telescope
delta2 Permutation
perm = VarSet -> Telescope -> SplitTel
splitTelescope VarSet
fv Telescope
delta

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

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

  in (Telescope
delta1, Telescope
delta2, Permutation
perm, Type
t', [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 types.
  -> [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.
  -> [(Int,(Term,Term))]                -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b  boundary.
  -> TCM (Type, Nat)
    -- ^ @Δ₁ → wtel → Δ₂′ → b′@ such that
    --     @[vs/wtel]wtel = as@ and
    --     @[vs/wtel]Δ₂′ = Δ₂@ and
    --     @[vs/wtel]b′ = b@.
    -- Plus the final number of with-arguments.
withFunctionType :: Telescope
-> [Arg (Term, EqualityView)]
-> Telescope
-> Type
-> [(Int, (Term, Term))]
-> TCM (Type, Int)
withFunctionType Telescope
delta1 [Arg (Term, EqualityView)]
vtys Telescope
delta2 Type
b [(Int, (Term, Term))]
bndry = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ do

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.abstract" Int
20 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 = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.abstract" Int
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x

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

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

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

  let nwithargs :: Int
nwithargs = [EqualityView] -> Int
countWithArgs (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg (Term, EqualityView)]
vtys)

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

  -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂"
  let bndry' :: [(Int, (Term, Term))]
bndry' = [(Int
i 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)) <- [(Int, (Term, Term))]
bndry, Int
i forall a. Ord a => a -> a -> Bool
>= Int
sd2]
        where sd2 :: Int
sd2 = forall a. Sized a => a -> Int
size Telescope
delta2
              lams :: Term -> Term
lams Term
u = forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs Telescope
wtel (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
delta2 Term
u)

  Type
d1wd2b <- Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
telePiPath_ Telescope
delta1 Type
wd2b [(Int, (Term, Term))]
bndry'

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

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

countWithArgs :: [EqualityView] -> Nat
countWithArgs :: [EqualityView] -> Int
countWithArgs = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Num a => EqualityView -> a
countArgs
  where
    countArgs :: EqualityView -> a
countArgs OtherType{}    = a
1
    countArgs IdiomType{}    = a
2
    countArgs EqualityType{} = a
2

-- | From a list of @with@ and @rewrite@ expressions and their types,
--   compute the list of final @with@ expressions (after expanding the @rewrite@s).
withArguments :: [Arg (Term, EqualityView)] ->
                 TCM [Arg Term]
withArguments :: [Arg (Term, EqualityView)] -> TCM Args
withArguments [Arg (Term, EqualityView)]
vtys = do
  [Args]
tss <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Arg (Term, EqualityView)]
vtys forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info (Term, EqualityView)
ts) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> [a] -> [b]
map (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info)) forall a b. (a -> b) -> a -> b
$ case (Term, EqualityView)
ts of
    (Term
v, OtherType Type
a) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term
v]
    (Term
prf, eqt :: EqualityView
eqt@(EqualityType Sort
s QName
_eq Args
_pars Arg Term
_t Arg Term
v Arg Term
_v')) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall e. Arg e -> e
unArg Arg Term
v, Term
prf]
    (Term
v, IdiomType Type
t) -> do
       Arg Term -> Term
mkRefl <- TCM (Arg Term -> Term)
getRefl
       forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term
v, Arg Term -> Term
mkRefl (forall a. a -> Arg a
defaultArg Term
v)]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Args]
tss)

-- | 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.
  -> [A.SpineClause]      -- ^ With-clauses.
  -> TCM [A.SpineClause]  -- ^ With-clauses flattened wrt. parent patterns.
buildWithFunction :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Substitution' Term
-> Permutation
-> Int
-> Int
-> [Clause' SpineLHS]
-> TCM [Clause' SpineLHS]
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Substitution' Term
withSub Permutation
perm Int
n1 Int
n [Clause' SpineLHS]
cs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause [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 (A.SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
allPs) [ProblemEq]
inheritedPats RHS
rhs WhereDeclarations
wh Bool
catchall) = do
      let ([NamedArg Pattern]
ps, [NamedArg Pattern]
wps)    = [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
splitOffTrailingWithPatterns [NamedArg Pattern]
allPs
          ([NamedArg Pattern]
wps0, [NamedArg Pattern]
wps1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
wps
          ps0 :: [NamedArg Pattern]
ps0          = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg forall {e}. Pattern' e -> Pattern' e
fromWithP) [NamedArg Pattern]
wps0
            where
            fromWithP :: Pattern' e -> Pattern' e
fromWithP (A.WithP PatInfo
_ Pattern' e
p) = Pattern' e
p
            fromWithP Pattern' e
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inheritedPats:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
        | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats
        ]
      ([ProblemEq]
strippedPats, [NamedArg Pattern]
ps') <- [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"strippedPats:" Int
2 forall a b. (a -> b) -> a -> b
$
                                  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
t)
                                       | A.ProblemEq Pattern
p Term
v Dom Type
t <- [ProblemEq]
strippedPats ]
      RHS
rhs <- [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
strippedPats RHS
rhs
      let ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n1 [NamedArg Pattern]
ps'
      let result :: Clause' SpineLHS
result = forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
ps1 forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps0 forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps2 forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
wps1)
                     ([ProblemEq]
inheritedPats forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
                     RHS
rhs WhereDeclarations
wh Bool
catchall
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"buildWithClause returns" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Clause' SpineLHS
result
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return Clause' SpineLHS
result

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


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

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

Example:

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

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

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

With function:

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

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

Resulting with-function clause is:

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

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

@
  ps = qs[ps']
@

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

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

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

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

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

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

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

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

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

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

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

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

        DefP{}  -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"with clauses not supported in the presence of hcomp patterns" -- TODO this should actually be impossible

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

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

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

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

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

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

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

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

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

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

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

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

          Pattern
_ -> forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
      where
        recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse Term
v = do
          -- caseMaybeM (liftTCM $ isPath t) (return ()) $ \ _ ->
          --   typeError $ GenericError $
          --     "With-clauses currently not supported under Path abstraction."

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

        mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
        mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
          Pattern -> NamedArg DeBruijnPattern -> TypeError
WithClausePatternMismatch (forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0) NamedArg DeBruijnPattern
q
        mismatchOrigin :: ProjOrigin -> ProjOrigin -> TCMT IO [NamedArg Pattern]
mismatchOrigin ProjOrigin
o ProjOrigin
o' = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ TCMT IO Doc
"With clause pattern"
          , forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p0
          , TCMT IO Doc
"is not an instance of its parent pattern"
          , forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"since the parent pattern is " forall a. [a] -> [a] -> [a]
++ forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o forall a. [a] -> [a] -> [a]
++
                   [Char]
" and the with clause pattern is " forall a. [a] -> [a] -> [a]
++ forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o'
          ]
        prettyProjOrigin :: ProjOrigin -> a
prettyProjOrigin ProjOrigin
ProjPrefix  = a
"a prefix projection"
        prettyProjOrigin ProjOrigin
ProjPostfix = a
"a postfix projection"
        prettyProjOrigin ProjOrigin
ProjSystem  = forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"inserting implicit"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern]
ps' forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps)
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            ]

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

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

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

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

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

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

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

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

  forall (m :: * -> *) a. Monad m => a -> m a
return DisplayForm
display
  where
    -- Ulf, 2014-02-19: We need to rename the module parameters as well! (issue1035)
    -- sub top ys wild = map term [0 .. m - 1] ++# raiseS (length qs)
    -- Andreas, 2015-10-28: Yes, but properly! (Issue 1407)
    sub :: Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
term [Int
0 .. Int
m forall a. Num a => a -> a -> a
+ Int
top forall a. Num a => a -> a -> a
- Int
1]
      where
        term :: Int -> Term
term Int
i = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
wild Int -> Term
var forall a b. (a -> b) -> a -> b
$ forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ Arg DeBruijnPattern -> Elim' DisplayTerm
toElim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 -> forall a. ProjOrigin -> QName -> Elim' a
I.Proj ProjOrigin
o QName
d
      DeBruijnPattern
p         -> forall a. Arg a -> Elim' a
I.Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p

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

    toTerm :: DeBruijnPattern -> DisplayTerm
    toTerm :: DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p = case PatternInfo -> PatOrigin
patOrigin forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p of
      PatOrigin
PatOSystem -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatOSplit  -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOVar{}  -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
      PatOrigin
PatODot    -> Term -> DisplayTerm
DDot 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 forall a b. (a -> b) -> a -> b
$ Int -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x -- TODO, should be an Elim' DisplayTerm ?
      ProjP ProjOrigin
_ QName
d  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      VarP PatternInfo
i DBPatVar
x -> Term -> DisplayTerm
DTerm  forall a b. (a -> b) -> a -> b
$ Int -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
      DotP PatternInfo
i Term
t -> Term -> DisplayTerm
DDot   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) forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms [NamedArg DeBruijnPattern]
ps
      LitP PatternInfo
i Literal
l -> Term -> DisplayTerm
DTerm  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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply 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 forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
      Term
t        -> Term -> DisplayTerm
DDot Term
t