{-# 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 = [Arg (Term, EqualityView)] -> VarSet
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 = Impossible -> Permutation -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm)
    -- Δ₁ ⊢ ρ : Δ₁Δ₂  (We know that as does not depend on Δ₂.)
    rho :: Substitution' Term
rho = Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Int -> Substitution' Term) -> Int -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
    -- Δ₁ ⊢ ρ ∘ π : Δ
    rhopi :: Substitution' Term
rhopi = Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' Term
rho Substitution' Term
pi

    -- We need Δ₁Δ₂ ⊢ t'
    t' :: Type
t' = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
pi Type
t
    -- and Δ₁ ⊢ vtys'
    vtys' :: [Arg (Term, EqualityView)]
vtys' = Substitution' (SubstArg [Arg (Term, EqualityView)])
-> [Arg (Term, EqualityView)] -> [Arg (Term, EqualityView)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Arg (Term, EqualityView)])
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 = Telescope -> TCM (Type, Int) -> TCM (Type, Int)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCM (Type, Int) -> TCM (Type, Int))
-> TCM (Type, Int) -> TCM (Type, Int)
forall a b. (a -> b) -> a -> b
$ do

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

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

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

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

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

  let nwithargs :: Int
nwithargs = [EqualityView] -> Int
countWithArgs ((Arg (Term, EqualityView) -> EqualityView)
-> [Arg (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((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) [Arg (Term, EqualityView)]
vtys)

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

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

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

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

countWithArgs :: [EqualityView] -> Nat
countWithArgs :: [EqualityView] -> Int
countWithArgs = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int)
-> ([EqualityView] -> [Int]) -> [EqualityView] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EqualityView -> Int) -> [EqualityView] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map 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

-- | 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 <- [Arg (Term, EqualityView)]
-> (Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Arg (Term, EqualityView)]
vtys ((Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args])
-> (Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args]
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info (Term, EqualityView)
ts) -> ([Term] -> Args) -> TCMT IO [Term] -> TCM Args
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> Arg Term) -> [Term] -> Args
forall a b. (a -> b) -> [a] -> [b]
map (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info)) (TCMT IO [Term] -> TCM Args) -> TCMT IO [Term] -> TCM Args
forall a b. (a -> b) -> a -> b
$ case (Term, EqualityView)
ts of
    (Term
v, OtherType Type
a) -> [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO 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')) -> [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Arg Term -> Term
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
       [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term
v, Arg Term -> Term
mkRefl (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v)]
  Args -> TCM Args
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Args] -> Args
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 = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> [Clause' SpineLHS] -> TCM [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) -> [a] -> m [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) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
wps
          ps0 :: [NamedArg Pattern]
ps0          = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> Pattern
forall {e}. Pattern' e -> Pattern' e
fromWithP) [NamedArg Pattern]
wps0
            where
            fromWithP :: Pattern' e -> Pattern' e
fromWithP (A.WithP PatInfo
_ Pattern' e
p) = Pattern' e
p
            fromWithP Pattern' e
_ = Pattern' e
forall a. HasCallStack => a
__IMPOSSIBLE__
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inheritedPats:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
        | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats
        ]
      ([ProblemEq]
strippedPats, [NamedArg Pattern]
ps') <- [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"strippedPats:" Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
                                  [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
t)
                                       | A.ProblemEq Pattern
p Term
v Dom Type
t <- [ProblemEq]
strippedPats ]
      RHS
rhs <- [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
strippedPats RHS
rhs
      let ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n1 [NamedArg Pattern]
ps'
      let result :: Clause' SpineLHS
result = SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux ([NamedArg Pattern] -> SpineLHS) -> [NamedArg Pattern] -> SpineLHS
forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
ps1 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps0 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps2 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
wps1)
                     ([ProblemEq]
inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
                     RHS
rhs WhereDeclarations
wh Bool
catchall
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"buildWithClause returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Clause' SpineLHS -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Clause' SpineLHS
result
        ]
      Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Clause' SpineLHS
result

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

    -- The stripped patterns computed by buildWithClause lives in the context
    -- of the top with-clause (of the current call to buildWithFunction). When
    -- we recurse we expect inherited patterns to live in the context
    -- of the innermost parent clause. Note that this makes them live in the
    -- context of the with-function arguments before any pattern matching. We
    -- need to update again once the with-clause patterns have been checked.
    -- This happens in Rules.Def.checkClause before calling checkRHS.
    permuteNamedDots :: A.SpineClause -> A.SpineClause
    permuteNamedDots :: Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots (A.Clause SpineLHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
catchall) =
      SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 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 <- [NamedArg Pattern] -> TCM [NamedArg Pattern]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg Pattern]
ps
  -- Ulf, 2016-11-16 Issue 2303: We need the module parameter
  -- instantiations from qs, so we make sure
  -- that t is the top-level type of the parent function and add patterns for
  -- the module parameters to ps before stripping.
  let paramPat :: Int -> DeBruijnPattern -> Pattern
paramPat Int
i DeBruijnPattern
_ = BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName (Name -> BindName) -> Name -> BindName
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Int -> Name
forall a. a -> [a] -> Int -> a
indexWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ [Name]
cxtNames Int
i
      ps' :: [NamedArg Pattern]
ps' = (Int -> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [Int] -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
 -> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> (Int
    -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> Int
-> NamedArg DeBruijnPattern
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> Pattern)
-> Named NamedName DeBruijnPattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> Pattern)
 -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> (Int -> DeBruijnPattern -> Pattern)
-> Int
-> Named NamedName DeBruijnPattern
-> Named NamedName Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DeBruijnPattern -> Pattern
paramPat) [Int
0..] (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
take Int
npars [NamedArg DeBruijnPattern]
qs) [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps
  [NamedArg Pattern]
psi <- ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps' Type
t
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"stripping patterns"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps')
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"psi = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
psi)
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"qs  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"perm= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
    ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          A.RecP PatInfo
_ [FieldAssignment' Pattern]
fs -> WriterT [ProblemEq] (TCMT IO) (Maybe Defn)
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> (Defn -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe Defn) -> WriterT [ProblemEq] (TCMT IO) (Maybe Defn)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe Defn) -> WriterT [ProblemEq] (TCMT IO) (Maybe Defn))
-> TCM (Maybe Defn) -> WriterT [ProblemEq] (TCMT IO) (Maybe Defn)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
d) WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch ((Defn -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> (Defn -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \ Defn
def -> do
            [NamedArg Pattern]
ps' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> Pattern)
-> [FieldAssignment' Pattern]
-> [Arg Name]
-> TCM [NamedArg Pattern]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (Pattern -> Name -> Pattern
forall a b. a -> b -> a
const (Pattern -> Name -> Pattern) -> Pattern -> Name -> Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) [FieldAssignment' Pattern]
fs
                                                 ((Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ 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
             [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
               TCMT IO Doc
"stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
             WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

        mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
        mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch = Telescope -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$
          Pattern -> NamedArg DeBruijnPattern -> TypeError
WithClausePatternMismatch (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0) NamedArg DeBruijnPattern
q
        mismatchOrigin :: ProjOrigin -> ProjOrigin -> TCM [NamedArg Pattern]
mismatchOrigin ProjOrigin
o ProjOrigin
o' = Telescope -> TCM [NamedArg Pattern] -> TCM [NamedArg Pattern]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (TCM [NamedArg Pattern] -> TCM [NamedArg Pattern])
-> (Doc -> TCM [NamedArg Pattern]) -> Doc -> TCM [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM [NamedArg Pattern]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [NamedArg Pattern])
-> (Doc -> TypeError) -> Doc -> TCM [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM [NamedArg Pattern])
-> TCMT IO Doc -> TCM [NamedArg Pattern]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ TCMT IO Doc
"With clause pattern"
          , NamedArg Pattern -> TCMT IO Doc
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"
          , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> TCMT IO [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]
          , [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]
"since the parent pattern is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                   [Char]
" and the with clause pattern is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> [Char]
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  = a
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

  -- Build the rhs of the display form.
  Term
wild <- TCMT IO Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_ TCMT IO Name -> (Name -> Term) -> TCM Term
forall (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) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta1) ([Int] -> ([Int], [Int])) -> [Int] -> ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ Permutation -> [Int] -> [Int]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
m
      ys :: [Maybe Int]
ys         = [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a]
reverse ((Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys0 [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ Int -> Maybe Int -> [Maybe Int]
forall a. Int -> a -> [a]
replicate Int
n Maybe Int
forall a. Maybe a
Nothing [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys1)
                   [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+)) [Int
0..Int
topInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
      rho :: Substitution' Term
rho        = Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild
      tqs :: [Elim' DisplayTerm]
tqs        = Substitution' (SubstArg [Elim' DisplayTerm])
-> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Elim' DisplayTerm])
rho [Elim' DisplayTerm]
tqs0
      -- Build the arguments to the with function.
      es :: [Elim' DisplayTerm]
es         = (Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
topArgs [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ [Elim' DisplayTerm]
tqs
      withArgs :: [Term]
withArgs   = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
      dt :: DisplayTerm
dt         = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp (QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
f [Elim' DisplayTerm]
es) ((Term -> DisplayTerm) -> [Term] -> [DisplayTerm]
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 [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i | Int
i <- Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
arity] DisplayTerm
dt

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

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

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

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

    toTerm :: DeBruijnPattern -> DisplayTerm
    toTerm :: DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p = case PatternInfo -> PatOrigin
patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Maybe PatternInfo -> PatternInfo
forall a. a -> Maybe a -> a
fromMaybe PatternInfo
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe PatternInfo -> PatternInfo)
-> Maybe PatternInfo -> PatternInfo
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p of
      PatOrigin
PatOSystem -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      PatOrigin
PatOSplit  -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
      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