    {-# OPTIONS_GHC -Wunused-imports #-}

    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 a. [a] -> 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 = (nameToArgName x, 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 = (stringToArgName "()", 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 = (stringToArgName "x", a) }
              | Bool
    otherwise                  -> Dom' t (ArgName, b)
    dom

    useNamesFromProblemEqs
      :: forall m. (PureTCM m, MonadFresh NameId m)
      => [ProblemEq] -> Telescope -> m Telescope
    useNamesFromProblemEqs :: forall (m :: * -> *).
    (PureTCM m, MonadFresh NameId 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (m Telescope -> m Telescope) -> m Telescope -> m Telescope
    forall a b. (a -> b) -> a -> b
    $ do
      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 [(Arg Name, PatVarPosition)]
    -> ([Maybe Name], [AsBinding])
    getUserVariableNames Telescope
    tel (IntMap [(Arg Name, PatVarPosition)]
     -> ([Maybe Name], [AsBinding]))
    -> (LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)])
    -> LeftoverPatterns
    -> ([Maybe Name], [AsBinding])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LeftoverPatterns -> IntMap [(Arg 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, MonadFresh NameId m) =>
    [ProblemEq] -> m LeftoverPatterns
    getLeftoverPatterns [ProblemEq]
    eqs
      let argNames = (Maybe Name -> Maybe ArgName) -> [Maybe Name] -> [Maybe ArgName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name -> ArgName) -> Maybe Name -> Maybe ArgName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> ArgName
    nameToArgName) [Maybe Name]
    names
      return $ renameTel argNames 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 a. [a] -> 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
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.init" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "initLHSState"
        , 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
    "delta = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    delta
        , 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
    "a     = " 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a)
        ]
      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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Telescope
    delta

      LHSState a -> TCMT IO (LHSState a)
    forall (m :: * -> *) a.
    (PureTCM m, MonadError TCErr m, MonadTrace m,
     MonadFresh NameId m) =>
    LHSState a -> m (LHSState a)
    updateProblemRest (LHSState a -> TCMT IO (LHSState a))
    -> LHSState a -> TCMT IO (LHSState a)
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> [NamedArg DeBruijnPattern]
    -> Problem a
    -> Arg Type
    -> [Maybe Int]
    -> Bool
    -> LHSState a
    forall a.
    Telescope
    -> [NamedArg DeBruijnPattern]
    -> Problem a
    -> Arg Type
    -> [Maybe Int]
    -> Bool
    -> LHSState a
    LHSState Telescope
    delta [NamedArg DeBruijnPattern]
    qs0 Problem a
    problem (ArgInfo -> Type -> Arg Type
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo
    defaultArgInfo { argInfoModality = unitModality }) Type
    a) [] Bool
    False

    -- | 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 Bool
    ixsplit) = Telescope -> m (LHSState a) -> m (LHSState 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
    tel0 (m (LHSState a) -> m (LHSState a))
    -> m (LHSState a) -> m (LHSState a)
    forall a b. (a -> b) -> a -> b
    $ do
      ps <- 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
      reportSDoc "tc.lhs.imp" 20 $
        "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
      -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
      let m = [NamedArg Pattern] -> Int
    forall a. [a] -> 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 gamma b, boundary) <- telViewUpToPathBoundary' m $ unArg a
      forM_ (zip ps (telToList gamma)) $ \(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      = [NamedArg Pattern] -> Telescope -> Telescope
    useNamesFromPattern [NamedArg Pattern]
    ps Telescope
    gamma
          n         = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel1
          (ps1,ps2) = splitAt n ps
          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       = Telescope -> Boundary -> [NamedArg DeBruijnPattern]
    forall a.
    DeBruijn a =>
    Telescope -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns Telescope
    tel1 Boundary
    boundary
          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       = Int -> Substitution' DeBruijnPattern
    forall a. Int -> Substitution' a
    raiseS Int
    n
      reportSDoc "tc.lhs.problem" 10 $ addContext tel0 $ vcat
        [ "checking lhs -- updated split problem:"
        , nest 2 $ vcat
          [ "ps    =" <+> fsep (map prettyA ps)
          , "a     =" <+> prettyTCM a
          , "tel1  =" <+> prettyTCM tel1
          , "ps1   =" <+> fsep (map prettyA ps1)
          , "ps2   =" <+> fsep (map prettyA ps2)
          , "b     =" <+> addContext tel1 (prettyTCM b)
          ]
        ]
      reportSDoc "tc.lhs.problem" 60 $ addContext tel0 $ vcat
        [ nest 2 $ vcat
          [ "ps    =" <+> (text . show) ps
          , "a     =" <+> (text . show) a
          , "tel1  =" <+> (text . show) tel1
          , "ps1   =" <+> (text . show) ps1
          , "ps2   =" <+> (text . show) ps2
          , "b     =" <+> (text . show) b
          , "qs1   =" <+> fsep (map pretty qs1)
          ]
        ]
      return $ LHSState
        { _lhsTel     = tel
        , _lhsOutPat  = applySubst tau qs0 ++ qs1
        , _lhsProblem = Problem
                       { _problemEqs      = applyPatSubst tau oldEqs ++ newEqs
                       , _problemRestPats = ps2
                       , _problemCont     = ret
                       }
        , _lhsTarget  = a $> b
        , _lhsPartialSplit = psplit
        , _lhsIndexedSplit = ixsplit
        }