{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.With where

import Prelude hiding ((!!))

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

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

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

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

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

import Agda.Utils.Impossible

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

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

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

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

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

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

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


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

withFunctionType
  :: Telescope                          -- ^ @Δ₁@                        context for types of with types.
  -> List1 (Arg (Term, EqualityView))   -- ^ @Δ₁,Δ₂ ⊢ vs : raise Δ₂ as@  with and rewrite-expressions and their type.
  -> Telescope                          -- ^ @Δ₁ ⊢ Δ₂@                   context extension to type with-expressions.
  -> Type                               -- ^ @Δ₁,Δ₂ ⊢ b@                 type of rhs.
  -> [(Int,(Term,Term))]                -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b  boundary.
  -> TCM (Type, Nat1)
    -- ^ @Δ₁ → 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
-> List1 (Arg (Term, EqualityView))
-> Telescope
-> Type
-> [(Int, (Term, Term))]
-> TCM (Type, Int)
withFunctionType Telescope
delta1 List1 (Arg (Term, EqualityView))
vtys Telescope
delta2 Type
b [(Int, (Term, Term))]
bndry = Telescope -> TCM (Type, Int) -> TCM (Type, Int)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCM (Type, Int) -> TCM (Type, Int))
-> TCM (Type, Int) -> TCM (Type, Int)
forall a b. (a -> b) -> a -> b
$ do

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

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

  d2b <- Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
telePiPath_ Telescope
delta2 Type
b [(Int, (Term, Term))]
bndry
  dbg 30 "Δ₂ → B" d2b
  d2b  <- normalise d2b
  dbg 30 "normal Δ₂ → B" d2b
  d2b  <- etaContract d2b
  dbg 30 "eta-contracted Δ₂ → B" d2b

  vtys <- etaContract =<< normalise vtys

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

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

  TelV wtel _ <- telViewUpTo nwithargs wd2b

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

  d1wd2b <- telePiPath_ delta1 wd2b bndry'

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

  return (d1wd2b, nwithargs)

countWithArgs :: List1 EqualityView -> Nat1
countWithArgs :: List1 EqualityView -> Int
countWithArgs = NonEmpty Int -> Int
forall a. Num a => NonEmpty a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (NonEmpty Int -> Int)
-> (List1 EqualityView -> NonEmpty Int)
-> List1 EqualityView
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EqualityView -> Int) -> List1 EqualityView -> NonEmpty Int
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Int
forall {a}. Num a => EqualityView -> a
countArgs
  where
    countArgs :: EqualityView -> a
countArgs OtherType{}    = a
1
    countArgs IdiomType{}    = a
2
    countArgs EqualityType{} = a
2

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

-- | Compute the clauses for the with-function given the original patterns.
buildWithFunction
  :: [Name]               -- ^ Names of the module parameters of the parent function.
  -> QName                -- ^ Name of the parent function.
  -> QName                -- ^ Name of the with-function.
  -> Type                 -- ^ Types of the parent function.
  -> Telescope            -- ^ Context of parent patterns.
  -> [NamedArg DeBruijnPattern] -- ^ Parent patterns.
  -> Nat                  -- ^ Number of module parameters in parent patterns
  -> Substitution         -- ^ Substitution from parent lhs to with function lhs
  -> Permutation          -- ^ Final permutation.
  -> Nat                  -- ^ Number of needed vars.
  -> Nat                  -- ^ Number of with expressions.
  -> List1 A.SpineClause  -- ^ With-clauses.
  -> TCM (List1 A.SpineClause) -- ^ With-clauses flattened wrt. parent patterns.
buildWithFunction :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Substitution' Term
-> Permutation
-> Int
-> Int
-> List1 (Clause' SpineLHS)
-> TCM (List1 (Clause' SpineLHS))
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Substitution' Term
withSub Permutation
perm Int
n1 Int
n List1 (Clause' SpineLHS)
cs = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> List1 (Clause' SpineLHS) -> TCM (List1 (Clause' SpineLHS))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause List1 (Clause' SpineLHS)
cs
  where
    -- Nested with-functions will iterate this function once for each parent clause.
    buildWithClause :: Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause (A.Clause (A.SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
allPs) [ProblemEq]
inheritedPats RHS
rhs WhereDeclarations
wh Bool
catchall) = do
      let ([NamedArg Pattern]
ps, [NamedArg Pattern]
wps)    = [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
splitOffTrailingWithPatterns [NamedArg Pattern]
allPs
          ([NamedArg Pattern]
wps0, [NamedArg Pattern]
wps1) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
wps
          ps0 :: [NamedArg Pattern]
ps0          = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> Pattern
forall {e}. Pattern' e -> Pattern' e
fromWithP) [NamedArg Pattern]
wps0
            where
            fromWithP :: Pattern' e -> Pattern' e
fromWithP (A.WithP PatInfo
_ Pattern' e
p) = Pattern' e
p
            fromWithP Pattern' e
_ = Pattern' e
forall a. HasCallStack => a
__IMPOSSIBLE__
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inheritedPats:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
        | A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats
        ]
      (strippedPats, 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
      reportSDoc "tc.with" 50 $ hang "strippedPats:" 2 $
                                  vcat [ prettyA p <+> "==" <+> prettyTCM v <+> (":" <+> prettyTCM t)
                                       | A.ProblemEq p v t <- strippedPats ]
      rhs <- buildRHS strippedPats rhs
      let (ps1, ps2) = splitAt n1 ps'
      let result = SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux ([NamedArg Pattern] -> SpineLHS) -> [NamedArg Pattern] -> SpineLHS
forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
ps1 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps0 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps2 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
wps1)
                     ([ProblemEq]
inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
                     RHS
rhs WhereDeclarations
wh Bool
catchall
      reportSDoc "tc.with" 20 $ vcat
        [ "buildWithClause returns" <+> prettyA result
        ]
      return result

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

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


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

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

Example:

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

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

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

With function:

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

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

Resulting with-function clause is:

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

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

@
  ps = qs[ps']
@

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

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

  -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function!
  (ps', strippedPats) <- runWriterT $ strip (Def parent []) t psi qs
  reportSDoc "tc.with.strip" 50 $ nest 2 $
    "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
  let psp = Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [NamedArg Pattern]
ps'
  reportSDoc "tc.with.strip" 10 $ vcat
    [ nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
    , nest 2 $ "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
    ]
  return (strippedPats, psp)
  where

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

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

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

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

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

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

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

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

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

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

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

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

         case namedArg p of

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

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

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

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

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

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

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

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

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

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

        mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
        mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch = Telescope -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$
          Pattern -> NamedArg DeBruijnPattern -> TypeError
WithClausePatternMismatch (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0) NamedArg DeBruijnPattern
q

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

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

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

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

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

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

          -- Insert implicit patterns (just for the constructor arguments)
          psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel'
          unless (size psi' == size tel') $ typeError $
            WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')

          -- Andreas, Ulf, 2016-06-01, Ulf's variant at issue #679
          -- Since instantiating the type with a constructor pattern
          -- can reveal more hidden arguments, we need to insert them here.
          psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t'

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

-- | 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.
  topArgs <- Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise Int
arity0 (Args -> Args) -> TCMT IO Args -> TCMT IO Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  let top    = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
topArgs
      arity  = Int
arity0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top

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

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

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

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

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

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

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

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

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