module Agda.TypeChecking.Rules.LHS.ProblemRest where

import Control.Monad
import Control.Monad.Except

import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute

import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Implicit

import Agda.Utils.Functor
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | Rename the variables in a telescope using the names from a given pattern.
--
--   If there are not at least as many patterns as entries as in the telescope,
--   the names of the remaining entries in the telescope are unchanged.
--   If there are too many patterns, there should be a type error later.
--
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
tel = ListTel -> Telescope
telFromList ((NamedArg Pattern
 -> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type))
-> [NamedArg Pattern] -> ListTel -> ListTel
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith NamedArg Pattern
-> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type)
forall {a} {e} {t} {b}.
Arg (Named a (Pattern' e))
-> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
ren [NamedArg Pattern]
ps ListTel
telList ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ ListTel
telRemaining)
  where
    telList :: ListTel
telList = Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
    telRemaining :: ListTel
telRemaining = Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop ([NamedArg Pattern] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Pattern]
ps) ListTel
telList -- telescope entries beyond patterns
    ren :: Arg (Named a (Pattern' e))
-> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
ren (Arg ArgInfo
ai (Named Maybe a
nm Pattern' e
p)) dom :: Dom' t (ArgName, b)
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
y, b
a) } =
      case Pattern' e
p of
        -- Andreas, 2017-10-12, issue #2803, also preserve user-written hidden names.
        -- However, not if the argument is named, because then the name in the telescope
        -- is significant for implicit insertion.
        A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}
          | Bool -> Bool
not (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x)
          , Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> Bool
|| (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
UserWritten Bool -> Bool -> Bool
&& Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing Maybe a
nm) ->
          Dom' t (ArgName, b)
dom{ unDom :: (ArgName, b)
unDom = (Name -> ArgName
nameToArgName Name
x, b
a) }
        A.AbsurdP{} | Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom -> Dom' t (ArgName, b)
dom{ unDom :: (ArgName, b)
unDom = (ArgName -> ArgName
stringToArgName ArgName
"()", b
a) }
        A.PatternSynP{} -> Dom' t (ArgName, b)
forall a. HasCallStack => a
__IMPOSSIBLE__  -- ensure there are no syns left
        -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x"
        Pattern' e
_ | Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> Bool
&& ArgName -> Bool
forall a. IsNoName a => a -> Bool
isNoName ArgName
y -> Dom' t (ArgName, b)
dom{ unDom :: (ArgName, b)
unDom = (ArgName -> ArgName
stringToArgName ArgName
"x", b
a) }
          | Bool
otherwise                  -> Dom' t (ArgName, b)
dom

useNamesFromProblemEqs
  :: forall m. PureTCM m
  => [ProblemEq] -> Telescope -> m Telescope
useNamesFromProblemEqs :: forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> Telescope -> m Telescope
useNamesFromProblemEqs [ProblemEq]
eqs Telescope
tel = Telescope -> m Telescope -> m Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m Telescope -> m Telescope) -> m Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ do
  [Maybe Name]
names <- ([Maybe Name], [AsBinding]) -> [Maybe Name]
forall a b. (a, b) -> a
fst (([Maybe Name], [AsBinding]) -> [Maybe Name])
-> (LeftoverPatterns -> ([Maybe Name], [AsBinding]))
-> LeftoverPatterns
-> [Maybe Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
tel (IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding]))
-> (LeftoverPatterns -> IntMap [(Name, PatVarPosition)])
-> LeftoverPatterns
-> ([Maybe Name], [AsBinding])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables (LeftoverPatterns -> [Maybe Name])
-> m LeftoverPatterns -> m [Maybe Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProblemEq] -> m LeftoverPatterns
forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs
  let argNames :: [Maybe ArgName]
argNames = (Maybe Name -> Maybe ArgName) -> [Maybe Name] -> [Maybe ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> ArgName) -> Maybe Name -> Maybe ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> ArgName
nameToArgName) [Maybe Name]
names
  Telescope -> m Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> m Telescope) -> Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> Telescope -> Telescope
renameTel [Maybe ArgName]
argNames Telescope
tel

useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom :: forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom = (a -> b -> a) -> [a] -> [b] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((a -> b -> a) -> [a] -> [b] -> [a])
-> (a -> b -> a) -> [a] -> [b] -> [a]
forall a b. (a -> b) -> a -> b
$ \a
x b
y -> Origin -> a -> a
forall a. LensOrigin a => Origin -> a -> a
setOrigin (b -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin b
y) a
x

-- | Are there any untyped user patterns left?
noProblemRest :: Problem a -> Bool
noProblemRest :: forall a. Problem a -> Bool
noProblemRest (Problem [ProblemEq]
_ [NamedArg Pattern]
rp LHSState a -> TCM a
_) = [NamedArg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
rp

-- | Construct an initial 'LHSState' from user patterns.
--   Example:
--   @
--
--      Case : {A : Set} → Maybe A → Set → Set → Set
--      Case nothing  B C = B
--      Case (just _) B C = C
--
--      sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool)
--      sample (just a) (just b) = true
--      sample (just a) nothing  = false
--      sample nothing           = true
--   @
--   The problem generated for the first clause of @sample@
--   with patterns @just a, just b@ would be:
--   @
--      lhsTel        = [A : Set, m : Maybe A]
--      lhsOutPat     = ["A", "m"]
--      lhsProblem    = Problem ["A" = _, "just a" = "a"]
--                              ["_", "just a"]
--                              ["just b"] []
--      lhsTarget     = "Case m Bool (Maybe A -> Bool)"
--   @
initLHSState
  :: Telescope             -- ^ The initial telescope @delta@ of parameters.
  -> [ProblemEq]           -- ^ The problem equations inherited from the parent clause (living in @delta@).
  -> [NamedArg A.Pattern]  -- ^ The user patterns.
  -> Type                  -- ^ The type the user patterns eliminate (living in @delta@).
  -> (LHSState a -> TCM a) -- ^ Continuation for when checking the patterns is complete.
  -> TCM (LHSState a)      -- ^ The initial LHS state constructed from the user patterns.
initLHSState :: forall a.
Telescope
-> [ProblemEq]
-> [NamedArg Pattern]
-> Type
-> (LHSState a -> TCM a)
-> TCM (LHSState a)
initLHSState Telescope
delta [ProblemEq]
eqs [NamedArg Pattern]
ps Type
a LHSState a -> TCM a
ret = do
  let problem :: Problem a
problem = [ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
forall a.
[ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
Problem [ProblemEq]
eqs [NamedArg Pattern]
ps LHSState a -> TCM a
ret
      qs0 :: [NamedArg DeBruijnPattern]
qs0     = Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
delta

  LHSState a -> TCM (LHSState a)
forall (m :: * -> *) a.
(PureTCM m, MonadError TCErr m, MonadTrace m,
 MonadFresh NameId m) =>
LHSState a -> m (LHSState a)
updateProblemRest (LHSState a -> TCM (LHSState a)) -> LHSState a -> TCM (LHSState a)
forall a b. (a -> b) -> a -> b
$ Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> LHSState a
forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> LHSState a
LHSState Telescope
delta [NamedArg DeBruijnPattern]
qs0 Problem a
problem (Type -> Arg Type
forall a. a -> Arg a
defaultArg Type
a) []

-- | Try to move patterns from the problem rest into the problem.
--   Possible if type of problem rest has been updated to a function type.
updateProblemRest
  :: forall m a. (PureTCM m, MonadError TCErr m, MonadTrace m, MonadFresh NameId m)
  => LHSState a -> m (LHSState a)
updateProblemRest :: forall (m :: * -> *) a.
(PureTCM m, MonadError TCErr m, MonadTrace m,
 MonadFresh NameId m) =>
LHSState a -> m (LHSState a)
updateProblemRest st :: LHSState a
st@(LHSState Telescope
tel0 [NamedArg DeBruijnPattern]
qs0 p :: Problem a
p@(Problem [ProblemEq]
oldEqs [NamedArg Pattern]
ps LHSState a -> TCM a
ret) Arg Type
a [Maybe Int]
psplit) = do
  [NamedArg Pattern]
ps <- Telescope -> m [NamedArg Pattern] -> m [NamedArg Pattern]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 (m [NamedArg Pattern] -> m [NamedArg Pattern])
-> m [NamedArg Pattern] -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps (Type -> m [NamedArg Pattern]) -> Type -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
a
  ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"insertImplicitPatternsT returned" 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 ((NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
  -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
  let m :: Int
m = [NamedArg Pattern] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamedArg Pattern] -> Int) -> [NamedArg Pattern] -> Int
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> Bool)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
-> (NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName))
-> NamedArg Pattern
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP) [NamedArg Pattern]
ps
  (TelV Telescope
gamma Type
b, Boundary
boundary) <- Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP Int
m (Type -> m (TelView, Boundary)) -> Type -> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
a
  [(NamedArg Pattern, Dom' Term (ArgName, Type))]
-> ((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([NamedArg Pattern]
-> ListTel -> [(NamedArg Pattern, Dom' Term (ArgName, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [NamedArg Pattern]
ps (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma)) (((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ())
-> ((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(NamedArg Pattern
p, Dom' Term (ArgName, Type)
a) ->
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (NamedArg Pattern -> Dom' Term (ArgName, Type) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg Pattern
p Dom' Term (ArgName, Type)
a) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern -> m () -> m ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
  let tel1 :: Telescope
tel1      = [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
gamma
      n :: Int
n         = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel1
      ([NamedArg Pattern]
ps1,[NamedArg Pattern]
ps2) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
ps
      tel :: Telescope
tel       = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0 ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel1
      qs1 :: [NamedArg DeBruijnPattern]
qs1       = Telescope -> Boundary -> [NamedArg DeBruijnPattern]
forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
tel1 Boundary
boundary
      newEqs :: [ProblemEq]
newEqs    = (Pattern -> Term -> Dom Type -> ProblemEq)
-> [Pattern] -> [Term] -> [Dom Type] -> [ProblemEq]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq
                    ((NamedArg Pattern -> Pattern) -> [NamedArg Pattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps1)
                    ((NamedArg DeBruijnPattern -> Term)
-> [NamedArg DeBruijnPattern] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Term
patternToTerm (DeBruijnPattern -> Term)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs1)
                    (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel1 [Dom Type] -> [NamedArg Pattern] -> [Dom Type]
forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
`useOriginFrom` [NamedArg Pattern]
ps1)
      tau :: Substitution' DeBruijnPattern
tau       = Int -> Substitution' DeBruijnPattern
forall a. Int -> Substitution' a
raiseS Int
n
  ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.problem" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking lhs -- updated split problem:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
      , TCMT IO Doc
"a     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
a
      , TCMT IO Doc
"tel1  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel1
      , TCMT IO Doc
"ps1   =" 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 ((NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps1)
      , TCMT IO Doc
"ps2   =" 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 ((NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps2)
      , TCMT IO Doc
"b     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel1 (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
      ]
    ]
  ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.problem" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> ([NamedArg Pattern] -> ArgName)
-> [NamedArg Pattern]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg Pattern] -> ArgName
forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps
      , TCMT IO Doc
"a     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Arg Type -> ArgName) -> Arg Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Type -> ArgName
forall a. Show a => a -> ArgName
show) Arg Type
a
      , TCMT IO Doc
"tel1  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Telescope -> ArgName) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ArgName
forall a. Show a => a -> ArgName
show) Telescope
tel1
      , TCMT IO Doc
"ps1   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> ([NamedArg Pattern] -> ArgName)
-> [NamedArg Pattern]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg Pattern] -> ArgName
forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps1
      , TCMT IO Doc
"ps2   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> ([NamedArg Pattern] -> ArgName)
-> [NamedArg Pattern]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg Pattern] -> ArgName
forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps2
      , TCMT IO Doc
"b     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Type -> ArgName) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ArgName
forall a. Show a => a -> ArgName
show) Type
b
      , TCMT IO Doc
"qs1   =" 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 ((NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
qs1)
      ]
    ]
  LHSState a -> m (LHSState a)
forall (m :: * -> *) a. Monad m => a -> m a
return (LHSState a -> m (LHSState a)) -> LHSState a -> m (LHSState a)
forall a b. (a -> b) -> a -> b
$ LHSState
    { _lhsTel :: Telescope
_lhsTel     = Telescope
tel
    , _lhsOutPat :: [NamedArg DeBruijnPattern]
_lhsOutPat  = Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' DeBruijnPattern
Substitution' (SubstArg [NamedArg DeBruijnPattern])
tau [NamedArg DeBruijnPattern]
qs0 [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
qs1
    , _lhsProblem :: Problem a
_lhsProblem = Problem
                   { _problemEqs :: [ProblemEq]
_problemEqs      = Substitution' DeBruijnPattern -> [ProblemEq] -> [ProblemEq]
forall a. TermSubst a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
tau [ProblemEq]
oldEqs [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
newEqs
                   , _problemRestPats :: [NamedArg Pattern]
_problemRestPats = [NamedArg Pattern]
ps2
                   , _problemCont :: LHSState a -> TCM a
_problemCont     = LHSState a -> TCM a
ret
                   }
    , _lhsTarget :: Arg Type
_lhsTarget  = Arg Type
a Arg Type -> Type -> Arg Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
b
    , _lhsPartialSplit :: [Maybe Int]
_lhsPartialSplit = [Maybe Int]
psplit
    }