{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.With where

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

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

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.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

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 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.
  -> [WithHiding (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 @π@
     , [WithHiding (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
-> [WithHiding (Term, EqualityView)]
-> (Telescope, Telescope, Permutation, Type,
    [WithHiding (Term, EqualityView)])
splitTelForWith Telescope
delta Type
t [WithHiding (Term, EqualityView)]
vtys = let
    -- Split the telescope into the part needed to type the with arguments
    -- and all the other stuff.
    fv :: VarSet
fv = [WithHiding (Term, EqualityView)] -> VarSet
forall t. Free t => t -> VarSet
allFreeVars [WithHiding (Term, EqualityView)]
vtys
    SplitTel Telescope
delta1 Telescope
delta2 Permutation
perm = VarSet -> Telescope -> SplitTel
splitTelescope VarSet
fv Telescope
delta

    -- Δ₁Δ₂ ⊢ π : Δ
    pi :: Substitution' Term
pi = Empty -> Permutation -> Substitution' Term
forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Permutation -> Permutation
reverseP Permutation
perm)
    -- Δ₁ ⊢ ρ : Δ₁Δ₂  (We know that as does not depend on Δ₂.)
    rho :: Substitution' a
rho = Empty -> Int -> Substitution' a
forall a. Empty -> Int -> Substitution' a
strengthenS Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Int -> Substitution' a) -> Int -> Substitution' a
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.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' Term
forall a. Substitution' a
rho Substitution' Term
pi

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

  in (Telescope
delta1, Telescope
delta2, Permutation
perm, Type
t', [WithHiding (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.
  -> [WithHiding (Term, EqualityView)]  -- ^ @Δ₁,Δ₂ ⊢ vs : raise Δ₂ as@  with and rewrite-expressions and their type.
  -> Telescope                          -- ^ @Δ₁ ⊢ Δ₂@                   context extension to type with-expressions.
  -> Type                               -- ^ @Δ₁,Δ₂ ⊢ b@                 type of rhs.
  -> 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
-> [WithHiding (Term, EqualityView)]
-> Telescope
-> Type
-> TCM (Type, Int)
withFunctionType Telescope
delta1 [WithHiding (Term, EqualityView)]
vtys Telescope
delta2 Type
b = Telescope -> TCM (Type, Int) -> TCM (Type, Int)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> 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

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

  let d2b :: Type
d2b = Telescope -> Type -> Type
telePi_ Telescope
delta2 Type
b
  Int -> VerboseKey -> Type -> TCMT IO ()
forall (m :: * -> *) a.
(MonadDebug m, PrettyTCM a) =>
Int -> VerboseKey -> a -> m ()
dbg Int
30 VerboseKey
"Δ₂ → B" Type
d2b
  Type
d2b  <- Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
d2b
  Int -> VerboseKey -> Type -> TCMT IO ()
forall (m :: * -> *) a.
(MonadDebug m, PrettyTCM a) =>
Int -> VerboseKey -> a -> m ()
dbg Int
30 VerboseKey
"normal Δ₂ → B" Type
d2b
  Type
d2b  <- Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Type
d2b
  Int -> VerboseKey -> Type -> TCMT IO ()
forall (m :: * -> *) a.
(MonadDebug m, PrettyTCM a) =>
Int -> VerboseKey -> a -> m ()
dbg Int
30 VerboseKey
"eta-contracted Δ₂ → B" Type
d2b

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

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

  (Type, Int) -> TCM (Type, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> Type -> Type
telePi_ Telescope
delta1 Type
wd2b, [EqualityView] -> Int
countWithArgs ((WithHiding (Term, EqualityView) -> EqualityView)
-> [WithHiding (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> WithHiding (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing) [WithHiding (Term, EqualityView)]
vtys))

countWithArgs :: [EqualityView] -> Nat
countWithArgs :: [EqualityView] -> Int
countWithArgs = [Int] -> Int
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 p. Num p => EqualityView -> p
countArgs
  where
    countArgs :: EqualityView -> p
countArgs OtherType{}    = p
1
    countArgs EqualityType{} = p
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 :: [WithHiding (Term, EqualityView)] -> [WithHiding Term]
withArguments :: [WithHiding (Term, EqualityView)] -> [WithHiding Term]
withArguments [WithHiding (Term, EqualityView)]
vtys = ((WithHiding (Term, EqualityView) -> [WithHiding Term])
 -> [WithHiding (Term, EqualityView)] -> [WithHiding Term])
-> [WithHiding (Term, EqualityView)]
-> (WithHiding (Term, EqualityView) -> [WithHiding Term])
-> [WithHiding Term]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (WithHiding (Term, EqualityView) -> [WithHiding Term])
-> [WithHiding (Term, EqualityView)] -> [WithHiding Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [WithHiding (Term, EqualityView)]
vtys ((WithHiding (Term, EqualityView) -> [WithHiding Term])
 -> [WithHiding Term])
-> (WithHiding (Term, EqualityView) -> [WithHiding Term])
-> [WithHiding Term]
forall a b. (a -> b) -> a -> b
$ ((Term, EqualityView) -> [Term])
-> WithHiding (Term, EqualityView) -> [WithHiding Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((Term, EqualityView) -> [Term])
 -> WithHiding (Term, EqualityView) -> [WithHiding Term])
-> ((Term, EqualityView) -> [Term])
-> WithHiding (Term, EqualityView)
-> [WithHiding Term]
forall a b. (a -> b) -> a -> b
$ \case
  (Term
v, OtherType Type
a) -> [Term
v]
  (Term
prf, eqt :: EqualityView
eqt@(EqualityType Sort
s QName
_eq [Arg Term]
_pars Arg Term
_t Arg Term
v Arg Term
_v')) -> [Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v, Term
prf]

-- | 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
-> [SpineClause]
-> TCM [SpineClause]
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 [SpineClause]
cs = (SpineClause -> TCMT IO SpineClause)
-> [SpineClause] -> TCM [SpineClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SpineClause -> TCMT IO SpineClause
buildWithClause [SpineClause]
cs
  where
    -- Nested with-functions will iterate this function once for each parent clause.
    buildWithClause :: SpineClause -> TCMT IO SpineClause
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__
      VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"inheritedPats:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
                                                               | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats ]
      ([ProblemEq]
strippedPats, [NamedArg Pattern]
ps') <- [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps
      VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> Int -> TCM Doc -> TCM Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCM Doc
"strippedPats:" Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
                                  [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"==" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
t)
                                       | A.ProblemEq Pattern
p Term
v Dom Type
t <- [ProblemEq]
strippedPats ]
      RHS
rhs <- [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
strippedPats RHS
rhs
      let ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n1 [NamedArg Pattern]
ps'
      let result :: SpineClause
result = SpineLHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> SpineClause
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
      VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"buildWithClause returns" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> SpineClause -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA SpineClause
result
        ]
      SpineClause -> TCMT IO SpineClause
forall (m :: * -> *) a. Monad m => a -> m a
return SpineClause
result

    buildRHS :: [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
_ rhs :: RHS
rhs@A.RHS{}                 = RHS -> TCMT IO RHS
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
    buildRHS [ProblemEq]
_ rhs :: RHS
rhs@RHS
A.AbsurdRHS             = RHS -> TCMT IO RHS
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
    buildRHS [ProblemEq]
_ (A.WithRHS QName
q [WithHiding Expr]
es [Clause]
cs)         = QName -> [WithHiding Expr] -> [Clause] -> RHS
A.WithRHS QName
q [WithHiding Expr]
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)
mapM ((SpineClause -> Clause
forall a b. LHSToSpine a b => b -> a
A.spineToLhs (SpineClause -> Clause)
-> (SpineClause -> SpineClause) -> SpineClause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpineClause -> SpineClause
permuteNamedDots) (SpineClause -> Clause)
-> (Clause -> TCMT IO SpineClause) -> Clause -> TCMT IO Clause
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> SpineClause -> TCMT IO SpineClause
buildWithClause (SpineClause -> TCMT IO SpineClause)
-> (Clause -> SpineClause) -> Clause -> TCMT IO SpineClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> SpineClause
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' Term -> [ProblemEq] -> [ProblemEq]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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 :: SpineClause -> SpineClause
permuteNamedDots (A.Clause SpineLHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
catchall) =
      SpineLHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> SpineClause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause SpineLHS
lhs (Substitution' Term -> [ProblemEq] -> [ProblemEq]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
withSub [ProblemEq]
strippedPats) RHS
rhs WhereDeclarations
wh Bool
catchall


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

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

Example:

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

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

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

With function:

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

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

Resulting with-function clause is:

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

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

@
  ps = qs[ps']
@

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

stripWithClausePatterns
  :: [Name]                   -- ^ __@cxtNames@__ names of the module parameters of the parent function
  -> QName                    -- ^ __@parent@__ name of the parent function.
  -> QName                    -- ^ __@f@__   name of with-function.
  -> Type                     -- ^ __@t@__   top-level type of the original function.
  -> Telescope                -- ^ __@Δ@__   context of patterns of parent function.
  -> [NamedArg DeBruijnPattern] -- ^ __@qs@__  internal patterns for original function.
  -> Nat                      -- ^ __@npars@__ number of module parameters in @qs@.
  -> Permutation              -- ^ __@π@__   permutation taking @vars(qs)@ to @support(Δ)@.
  -> [NamedArg A.Pattern]     -- ^ __@ps@__  patterns in with clause (eliminating type @t@).
  -> TCM ([A.ProblemEq], [NamedArg A.Pattern]) -- ^ __@ps'@__ patterns for with function (presumably of type @Δ@).
stripWithClausePatterns :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
parent QName
f Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps = do
  -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074)
  [NamedArg Pattern]
ps <- [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 -> p -> Pattern' e
paramPat Int
i p
_ = BindName -> Pattern' e
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern' e) -> BindName -> Pattern' e
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 (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 (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
forall p e. Int -> p -> Pattern' e
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]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps' Type
t
  VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"stripping patterns"
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"t   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCM Doc) -> [NamedArg Pattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCM Doc) -> [NamedArg Pattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps')
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"psi = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCM Doc) -> [NamedArg Pattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
psi)
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"qs  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCM Doc)
-> [NamedArg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (DeBruijnPattern -> TCM Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"perm= " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Permutation -> VerboseKey
forall a. Show a => a -> VerboseKey
show Permutation
perm)
    ]

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

    setVarArgInfo :: DBPatVar -> a -> a
setVarArgInfo DBPatVar
x a
p = Origin -> a -> a
forall a. LensOrigin a => Origin -> a -> a
setOrigin (a -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin a
p) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ ArgInfo -> a -> a
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (DBPatVar -> ArgInfo
varArgInfo DBPatVar
x) a
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] TCM [NamedArg Pattern]
strip Term
self Type
t [] qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
_ : [NamedArg DeBruijnPattern]
_) = do
      VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
15 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"strip (out of A.Patterns)"
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"qs  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCM Doc)
-> [NamedArg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (DeBruijnPattern -> TCM Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"self=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"t   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        ]
      -- Andreas, 2015-06-11, issue 1551:
      -- As the type t develops, we need to insert more implicit patterns,
      -- due to copatterns / flexible arity.
      [NamedArg Pattern]
ps <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [] Type
t
      if [NamedArg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
ps then
        TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Too few arguments given in with-clause"
       else Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] TCM [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] TCM () -> WriterT [ProblemEq] TCM ()
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] TCM () -> WriterT [ProblemEq] TCM ())
-> WriterT [ProblemEq] TCM () -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
        TypeError -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM ())
-> TypeError -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Too many arguments given in with-clause"
      [NamedArg Pattern] -> WriterT [ProblemEq] TCM [NamedArg Pattern]
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] TCM (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] TCM ()
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] TCM [NamedArg Pattern]
strip Term
self Type
t ((Named NamedName Pattern -> Named NamedName Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern
p Pattern -> Named NamedName Pattern -> Named NamedName Pattern
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] TCM (NamedArg Pattern)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (NamedArg Pattern)
 -> WriterT [ProblemEq] TCM (NamedArg Pattern))
-> TCM (NamedArg Pattern)
-> WriterT [ProblemEq] TCM (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)
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)
traverse) Pattern -> TCMT IO Pattern
expandLitPattern NamedArg Pattern
p0
      VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
15 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"strip"
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps0 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCM Doc) -> [NamedArg Pattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps0)
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"exp =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NamedArg Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"qs0 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Monad m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCM Doc)
-> [NamedArg DeBruijnPattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (DeBruijnPattern -> TCM Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs0)
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"self=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
self
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"t   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 NonEmpty 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] TCM [NamedArg Pattern]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> ProjOrigin -> TCM [NamedArg Pattern]
forall (m :: * -> *) b.
(IsString (m Doc), MonadError TCErr m, MonadAddContext m,
 MonadStConcreteNames m, HasBuiltins m, MonadReduce m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 Null (m Doc), Semigroup (m Doc)) =>
ProjOrigin -> ProjOrigin -> m b
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] TCM QName
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM QName -> WriterT [ProblemEq] TCM QName)
-> TCM QName -> WriterT [ProblemEq] TCM QName
forall a b. (a -> b) -> a -> b
$ QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
            Bool
found <- NonEmpty QName
-> (QName -> WriterT [ProblemEq] TCM Bool)
-> WriterT [ProblemEq] TCM Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM NonEmpty QName
ds ((QName -> WriterT [ProblemEq] TCM Bool)
 -> WriterT [ProblemEq] TCM Bool)
-> (QName -> WriterT [ProblemEq] TCM Bool)
-> WriterT [ProblemEq] TCM Bool
forall a b. (a -> b) -> a -> b
$ \ QName
d' -> TCM Bool -> WriterT [ProblemEq] TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT [ProblemEq] TCM Bool)
-> TCM Bool -> WriterT [ProblemEq] TCM 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 (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] TCM [NamedArg Pattern]
forall a. WriterT [ProblemEq] TCM a
mismatch else do
              (Term
self1, Type
t1, [NamedArg Pattern]
ps) <- TCM (Term, Type, [NamedArg Pattern])
-> WriterT [ProblemEq] TCM (Term, Type, [NamedArg Pattern])
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Term, Type, [NamedArg Pattern])
 -> WriterT [ProblemEq] TCM (Term, Type, [NamedArg Pattern]))
-> TCM (Term, Type, [NamedArg Pattern])
-> WriterT [ProblemEq] TCM (Term, Type, [NamedArg Pattern])
forall a b. (a -> b) -> a -> b
$ do
                Type
t <- Type -> TCMT IO 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 :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug 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]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps Type
t1
                (Term, Type, [NamedArg Pattern])
-> TCM (Term, Type, [NamedArg Pattern])
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
self1, Type
t1, [NamedArg Pattern]
ps)
              Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
strip Term
self1 Type
t1 [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs
          Maybe (ProjOrigin, AmbiguousQName)
Nothing -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a. WriterT [ProblemEq] TCM 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
forall a. (LensOrigin a, LensArgInfo a) => DBPatVar -> a -> a
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] TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))

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

        IApplyP{}  -> TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"with clauses not supported in the presence of Path patterns" -- TODO maybe we can support them now?
        DefP{}  -> TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TypeError -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"with clauses not supported in the presence of hcomp patterns" -- TODO this should actually be impossible

        DotP PatternInfo
o Term
v  -> do
          (Dom Type
a, Abs Type
_) <- Type -> WriterT [ProblemEq] TCM (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
          [ProblemEq] -> WriterT [ProblemEq] TCM ()
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]
          (NamedArg Pattern -> NamedArg Pattern
makeImplicitP NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
recurse Term
v

        q' :: DeBruijnPattern
q'@(ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
qs') -> do
         VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
60 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
           TCM Doc
"parent pattern is constructor " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
         (Dom Type
a, Abs Type
b) <- Type -> WriterT [ProblemEq] TCM (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] TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> WriterT [ProblemEq] TCM Term)
-> TCM Term -> WriterT [ProblemEq] TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (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 :: [Arg Term]
us = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
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] TCM (Either SigError ConHead)
-> WriterT [ProblemEq] TCM ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TCM (Either SigError ConHead)
-> WriterT [ProblemEq] TCM (Either SigError ConHead)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Either SigError ConHead)
 -> WriterT [ProblemEq] TCM (Either SigError ConHead))
-> TCM (Either SigError ConHead)
-> WriterT [ProblemEq] TCM (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] TCM ()
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 NonEmpty QName
cs')) [NamedArg Expr]
es -> do
                  [ConHead]
cs' <- TCM [ConHead] -> WriterT [ProblemEq] TCM [ConHead]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] TCM [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] TCM [ConHead]
forall a b. (a -> b) -> a -> b
$ ([SigError], [ConHead]) -> [ConHead]
forall a b. (a, b) -> b
snd (([SigError], [ConHead]) -> [ConHead])
-> ([Either SigError ConHead] -> ([SigError], [ConHead]))
-> [Either SigError ConHead]
-> [ConHead]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either SigError ConHead] -> ([SigError], [ConHead])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either SigError ConHead] -> [ConHead])
-> TCMT IO [Either SigError ConHead] -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> [QName] -> TCMT IO [Either SigError ConHead]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM (Either SigError ConHead)
getConForm (NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
cs')
                  Bool -> WriterT [ProblemEq] TCM () -> WriterT [ProblemEq] TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConHead -> [ConHead] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ConHead
c [ConHead]
cs') WriterT [ProblemEq] TCM ()
forall a. WriterT [ProblemEq] TCM a
mismatch
                  [NamedArg Pattern] -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern] -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> [NamedArg Pattern] -> WriterT [ProblemEq] TCM [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 (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 (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] TCM [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern] -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> [NamedArg Pattern] -> WriterT [ProblemEq] TCM [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 (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
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' :: [Arg (Named name (Pattern' e))]
ps' = (NamedArg DeBruijnPattern -> Arg (Named name (Pattern' e)))
-> [NamedArg DeBruijnPattern] -> [Arg (Named name (Pattern' e))]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' e -> Named name (Pattern' e)
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named name (Pattern' e)
-> NamedArg DeBruijnPattern -> Arg (Named name (Pattern' e))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
forall name e. [Arg (Named name (Pattern' e))]
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] TCM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP BindName
x) (DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
q') Dom Type
a]
            let ps' :: [Arg (Named name (Pattern' e))]
ps' = (NamedArg DeBruijnPattern -> Arg (Named name (Pattern' e)))
-> [NamedArg DeBruijnPattern] -> [Arg (Named name (Pattern' e))]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' e -> Named name (Pattern' e)
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named name (Pattern' e)
-> NamedArg DeBruijnPattern -> Arg (Named name (Pattern' e))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
            QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
forall name e. [Arg (Named name (Pattern' e))]
ps'

          A.ConP ConPatInfo
_ (A.AmbQ NonEmpty 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] TCM [ConHead]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] TCM [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] TCM [ConHead]
forall a b. (a -> b) -> a -> b
$ ([SigError], [ConHead]) -> [ConHead]
forall a b. (a, b) -> b
snd (([SigError], [ConHead]) -> [ConHead])
-> ([Either SigError ConHead] -> ([SigError], [ConHead]))
-> [Either SigError ConHead]
-> [ConHead]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either SigError ConHead] -> ([SigError], [ConHead])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either SigError ConHead] -> [ConHead])
-> TCMT IO [Either SigError ConHead] -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> [QName] -> TCMT IO [Either SigError ConHead]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM (Either SigError ConHead)
getConForm (NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
cs')
            Bool -> WriterT [ProblemEq] TCM () -> WriterT [ProblemEq] TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConHead -> [ConHead] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ConHead
c [ConHead]
cs') WriterT [ProblemEq] TCM ()
forall a. WriterT [ProblemEq] TCM a
mismatch
            -- Strip the subpatterns ps' and then continue.
            QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'

          A.RecP PatInfo
_ [FieldAssignment' Pattern]
fs -> WriterT [ProblemEq] TCM (Maybe Defn)
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
-> (Defn -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe Defn) -> WriterT [ProblemEq] TCM (Maybe Defn)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe Defn) -> WriterT [ProblemEq] TCM (Maybe Defn))
-> TCM (Maybe Defn) -> WriterT [ProblemEq] TCM (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] TCM [NamedArg Pattern]
forall a. WriterT [ProblemEq] TCM a
mismatch ((Defn -> WriterT [ProblemEq] TCM [NamedArg Pattern])
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> (Defn -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \ Defn
def -> do
            [NamedArg Pattern]
ps' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> Pattern)
-> [FieldAssignment' Pattern]
-> [Arg Name]
-> TCM [NamedArg Pattern]
forall a.
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFields 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' Term Name -> Arg Name) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term Name] -> [Arg Name]) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term Name]
recordFieldNames Defn
def)
            QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
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
             VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" Int
10 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
               TCM Doc
"stripWithClausePatterns: encountered pattern synonym " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
             WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

          Pattern
p -> do
           VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
60 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
             VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"with clause pattern is  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Pattern -> VerboseKey
forall a. Show a => a -> VerboseKey
show Pattern
p
           WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a. WriterT [ProblemEq] TCM a
mismatch

        LitP PatternInfo
_ Literal
lit -> case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of
          A.LitP Literal
lit' | Literal
lit Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
lit' -> Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit
          A.WildP{}                 -> Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] TCM [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
             VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" Int
10 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
               TCM Doc
"stripWithClausePatterns: encountered pattern synonym " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
             WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__

          Pattern
_ -> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a. WriterT [ProblemEq] TCM a
mismatch
      where
        recurse :: Term -> WriterT [ProblemEq] TCM [NamedArg Pattern]
recurse Term
v = do
          WriterT [ProblemEq] TCM (Maybe (Dom Type, Abs Type))
-> WriterT [ProblemEq] TCM ()
-> ((Dom Type, Abs Type) -> WriterT [ProblemEq] TCM ())
-> WriterT [ProblemEq] TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe (Dom Type, Abs Type))
-> WriterT [ProblemEq] TCM (Maybe (Dom Type, Abs Type))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe (Dom Type, Abs Type))
 -> WriterT [ProblemEq] TCM (Maybe (Dom Type, Abs Type)))
-> TCM (Maybe (Dom Type, Abs Type))
-> WriterT [ProblemEq] TCM (Maybe (Dom Type, Abs Type))
forall a b. (a -> b) -> a -> b
$ Type -> TCM (Maybe (Dom Type, Abs Type))
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
t) (() -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (((Dom Type, Abs Type) -> WriterT [ProblemEq] TCM ())
 -> WriterT [ProblemEq] TCM ())
-> ((Dom Type, Abs Type) -> WriterT [ProblemEq] TCM ())
-> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Dom Type, Abs Type)
_ ->
            TypeError -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM ())
-> TypeError -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$
              VerboseKey
"With-clauses currently not supported under Path abstraction."

          Type
t' <- Type -> Term -> WriterT [ProblemEq] TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
piApplyM Type
t Term
v
          Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
strip (Term
self Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
v) Type
t' [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

        mismatch :: WriterT [ProblemEq] TCM a
mismatch = Telescope -> WriterT [ProblemEq] TCM a -> WriterT [ProblemEq] TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (WriterT [ProblemEq] TCM a -> WriterT [ProblemEq] TCM a)
-> WriterT [ProblemEq] TCM a -> WriterT [ProblemEq] TCM a
forall a b. (a -> b) -> a -> b
$ TypeError -> WriterT [ProblemEq] TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM a)
-> TypeError -> WriterT [ProblemEq] TCM 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 -> m b
mismatchOrigin ProjOrigin
o ProjOrigin
o' = Telescope -> m b -> m b
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (m b -> m b) -> (Doc -> m b) -> Doc -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> m b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m b) -> (Doc -> TypeError) -> Doc -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> m b) -> m Doc -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
          [ m Doc
"With clause pattern"
          , NamedArg Pattern -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p0
          , m Doc
"is not an instance of its parent pattern"
          , [Doc] -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]
          , VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> m Doc) -> VerboseKey -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"since the parent pattern is " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> VerboseKey
forall p. IsString p => ProjOrigin -> p
prettyProjOrigin ProjOrigin
o VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                   VerboseKey
" and the with clause pattern is " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> VerboseKey
forall p. IsString p => ProjOrigin -> p
prettyProjOrigin ProjOrigin
o'
          ]
        prettyProjOrigin :: ProjOrigin -> p
prettyProjOrigin ProjOrigin
ProjPrefix  = p
"a prefix projection"
        prettyProjOrigin ProjOrigin
ProjPostfix = p
"a postfix projection"
        prettyProjOrigin ProjOrigin
ProjSystem  = p
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- | Make an ImplicitP, keeping arg. info.
        makeImplicitP :: NamedArg A.Pattern -> NamedArg A.Pattern
        makeImplicitP :: NamedArg Pattern -> NamedArg Pattern
makeImplicitP = (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
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
stripConP QName
d [Arg Term]
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] TCM 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 -> [Arg Term] -> Type
`piApply` Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
np [Arg Term]
us
          TelV Telescope
tel' Type
_ <- TCM (TelV Type) -> WriterT [ProblemEq] TCM (TelV Type)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (TelV Type) -> WriterT [ProblemEq] TCM (TelV Type))
-> TCM (TelV Type) -> WriterT [ProblemEq] TCM (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCM (TelV Type)
telViewPath Type
ct'
          -- (TelV tel' _, _boundary) <- liftTCM $ telViewPathBoundaryP ct'

          VerboseKey -> Int -> TCM Doc -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.strip" Int
20 (TCM Doc -> WriterT [ProblemEq] TCM ())
-> TCM Doc -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$
            [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ TCM Doc
"ct  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ct
                 , TCM Doc
"ct' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ct'
                 , TCM Doc
"np  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
np)
                 , TCM Doc
"us  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Arg Term -> TCM Doc) -> [Arg Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
us)
                 , TCM Doc
"us' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Arg Term -> TCM Doc) -> [Arg Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Arg Term] -> [TCM Doc]) -> [Arg Term] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
np [Arg Term]
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 -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
absApp (Int -> Abs Type -> Abs Type
forall t a. Subst t a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Abs Type
b) Term
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 t a. Subst t a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Term
self) Term
v  -- Issue 1546

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

          -- Insert implicit patterns (just for the constructor arguments)
          [NamedArg Pattern]
psi' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps' Telescope
tel'
          Bool -> WriterT [ProblemEq] TCM () -> WriterT [ProblemEq] TCM ()
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] TCM () -> WriterT [ProblemEq] TCM ())
-> WriterT [ProblemEq] TCM () -> WriterT [ProblemEq] TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> WriterT [ProblemEq] TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] TCM ())
-> TypeError -> WriterT [ProblemEq] TCM ()
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] TCM [NamedArg Pattern]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
 -> WriterT [ProblemEq] TCM [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] TCM [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [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] TCM [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.
  [Arg Term]
topArgs <- Int -> [Arg Term] -> [Arg Term]
forall t a. Subst t a => Int -> a -> a
raise Int
arity0 ([Arg Term] -> [Arg Term])
-> TCMT IO [Arg Term] -> TCMT IO [Arg Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
  let top :: Int
top    = [Arg Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
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' Term -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [Elim' DisplayTerm]
tqs0
      -- Build the arguments to the with function.
      es :: [Elim' DisplayTerm]
es         = (Arg Term -> Elim' DisplayTerm)
-> [Arg Term] -> [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) [Arg Term]
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 (Int -> Elim' Term -> Elims
forall a. Int -> a -> [a]
replicate Int
arity (Elim' Term -> Elims) -> Elim' Term -> Elims
forall a b. (a -> b) -> a -> b
$ 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
0) DisplayTerm
dt

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

  DisplayForm -> TCM DisplayForm
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 -> Bool) -> [Maybe Int] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [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 (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 (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 DeBruijnPattern
p of
      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   -> QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
d [] -- WRONG. TODO: convert spine to non-spine ... DDef d . defaultArg
      VarP PatternInfo
i DBPatVar
x -> case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOrigin
PatODot -> Term -> DisplayTerm
DDot  (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
        PatOrigin
_       -> 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 -> case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOVar{} | Var Int
i [] <- Term
t -> Term -> DisplayTerm
DTerm Term
t
        PatOrigin
_                         -> Term -> DisplayTerm
DDot   (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term
t
      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
_ 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