    {-| SplitClause and CoverResult types.
     -}

    module Agda.TypeChecking.Coverage.SplitClause where

    import Prelude hiding (null, (!!))  -- do not use partial functions like !!

    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet

    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Syntax.Internal hiding (DataOrRecord)

    import Agda.TypeChecking.Coverage.Match
    import Agda.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Warnings

    import Agda.Interaction.Options

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.WithDefault

    import Agda.Utils.Impossible

    data SplitClause = SClause
      { SplitClause -> Telescope
    scTel    :: Telescope
        -- ^ Type of variables in @scPats@.
      , SplitClause -> [NamedArg SplitPattern]
    scPats   :: [NamedArg SplitPattern]
        -- ^ The patterns leading to the currently considered branch of
        --   the split tree.
      , SplitClause -> Substitution' SplitPattern
    scSubst  :: Substitution' SplitPattern
        -- ^ Substitution from 'scTel' to old context.
        --   Only needed directly after split on variable:
        --   * To update 'scTarget'
        --   * To rename other split variables when splitting on
        --     multiple variables.
        --   @scSubst@ is not ``transitive'', i.e., does not record
        --   the substitution from the original context to 'scTel'
        --   over a series of splits.  It is freshly computed
        --   after each split by 'computeNeighborhood'; also
        --   'splitResult', which does not split on a variable,
        --   should reset it to the identity 'idS', lest it be
        --   applied to 'scTarget' again, leading to Issue 1294.
      , SplitClause -> Map CheckpointId Substitution
    scCheckpoints :: Map CheckpointId Substitution
        -- ^ We need to keep track of the module parameter checkpoints for the
        -- clause for the purpose of inferring missing instance clauses.
      , SplitClause -> Maybe (Dom Type)
    scTarget :: Maybe (Dom Type)
        -- ^ The type of the rhs, living in context 'scTel'.
        --   'fixTargetType' computes the new 'scTarget' by applying
        --   substitution 'scSubst'.
      }

    data UnifyEquiv = UE { UnifyEquiv -> Telescope
    infoTel0 :: Telescope          -- Γ0
                         , UnifyEquiv -> Telescope
    infoTel :: Telescope           -- Γ'
                         , UnifyEquiv -> Telescope
    infoEqTel :: Telescope         -- Γ0 ⊢ Δ
                         , UnifyEquiv -> [Term]
    infoEqLHS :: [Term]            -- Γ0 ⊢ us : Δ
                         , UnifyEquiv -> [Term]
    infoEqRHS :: [Term]            -- Γ0 ⊢ vs : Δ
                         , UnifyEquiv -> PatternSubstitution
    infoRho :: PatternSubstitution -- Γ' ⊢ ρ : Γ0
                                                          -- Γ = Γ0,(φ : I),(eqs : Paths Δ us vs)
                                                          -- Γ' ⊢ ρ,i1,refls : Γ
                         , UnifyEquiv -> Substitution
    infoTau :: Substitution        -- Γ  ⊢ τ           : Γ'
                         , UnifyEquiv -> Substitution
    infoLeftInv :: Substitution    -- Γ | (i : I) ⊢ leftInv : Γ
                         -- leftInv[i=0] = ρ[τ],i1s,refls
                         -- leftInv[i=1] = idS
                         }
                      deriving Int -> UnifyEquiv -> ShowS
    [UnifyEquiv] -> ShowS
    UnifyEquiv -> String
    (Int -> UnifyEquiv -> ShowS)
    -> (UnifyEquiv -> String)
    -> ([UnifyEquiv] -> ShowS)
    -> Show UnifyEquiv
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnifyEquiv -> ShowS
    showsPrec :: Int -> UnifyEquiv -> ShowS
    $cshow :: UnifyEquiv -> String
    show :: UnifyEquiv -> String
    $cshowList :: [UnifyEquiv] -> ShowS
    showList :: [UnifyEquiv] -> ShowS
    Show

    data IInfo = TheInfo UnifyEquiv | NoInfo deriving Int -> IInfo -> ShowS
    [IInfo] -> ShowS
    IInfo -> String
    (Int -> IInfo -> ShowS)
    -> (IInfo -> String) -> ([IInfo] -> ShowS) -> Show IInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IInfo -> ShowS
    showsPrec :: Int -> IInfo -> ShowS
    $cshow :: IInfo -> String
    show :: IInfo -> String
    $cshowList :: [IInfo] -> ShowS
    showList :: [IInfo] -> ShowS
    Show

    -- | A @Covering@ is the result of splitting a 'SplitClause'.
    data Covering = Covering
      { Covering -> Arg Int
    covSplitArg     :: Arg Nat
         -- ^ De Bruijn level (counting dot patterns) of argument we split on.
      , Covering -> [(SplitTag, (SplitClause, IInfo))]
    covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]
          -- ^ Covering clauses, indexed by constructor/literal these clauses share.
      }

    -- | Project the split clauses out of a covering.
    splitClauses :: Covering -> [SplitClause]
    splitClauses :: Covering -> [SplitClause]
    splitClauses (Covering Arg Int
    _ [(SplitTag, (SplitClause, IInfo))]
    qcs) = ((SplitTag, (SplitClause, IInfo)) -> SplitClause)
    -> [(SplitTag, (SplitClause, IInfo))] -> [SplitClause]
    forall a b. (a -> b) -> [a] -> [b]
    map ((SplitClause, IInfo) -> SplitClause
    forall a b. (a, b) -> a
    fst ((SplitClause, IInfo) -> SplitClause)
    -> ((SplitTag, (SplitClause, IInfo)) -> (SplitClause, IInfo))
    -> (SplitTag, (SplitClause, IInfo))
    -> SplitClause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SplitTag, (SplitClause, IInfo)) -> (SplitClause, IInfo)
    forall a b. (a, b) -> b
    snd) [(SplitTag, (SplitClause, IInfo))]
    qcs

    -- | Create a split clause from a clause in internal syntax. Used by make-case.
    clauseToSplitClause :: Clause -> SplitClause
    clauseToSplitClause :: Clause -> SplitClause
    clauseToSplitClause Clause
    cl = SClause
      { scTel :: Telescope
    scTel    = Clause -> Telescope
    clauseTel Clause
    cl
      , scPats :: [NamedArg SplitPattern]
    scPats   = [NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern]
    toSplitPatterns ([NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern]
    forall a b. (a -> b) -> a -> b
    $ Clause -> [NamedArg (Pattern' DBPatVar)]
    namedClausePats Clause
    cl
      , scSubst :: Substitution' SplitPattern
    scSubst  = Substitution' SplitPattern
    forall a. Substitution' a
    idS  -- Andreas, 2014-07-15  TODO: Is this ok?
      , scCheckpoints :: Map CheckpointId Substitution
    scCheckpoints = Map CheckpointId Substitution
    forall k a. Map k a
    Map.empty -- #2996: not __IMPOSSIBLE__ for debug printing
      , scTarget :: Maybe (Dom Type)
    scTarget = Arg Type -> Dom Type
    forall a. Arg a -> Dom a
    domFromArg (Arg Type -> Dom Type) -> Maybe (Arg Type) -> Maybe (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Clause -> Maybe (Arg Type)
    clauseType Clause
    cl
      }

    ---------------------------------------------
    -- Record type for the results of @cover@
    ---------------------------------------------

    data CoverResult = CoverResult
      { CoverResult -> SplitTree
    coverSplitTree       :: SplitTree
      , CoverResult -> IntSet
    coverUsedClauses     :: IntSet -- Set Nat
      , CoverResult -> [(Telescope, [NamedArg (Pattern' DBPatVar)])]
    coverMissingClauses  :: [(Telescope, [NamedArg DeBruijnPattern])]
      , CoverResult -> [Clause]
    coverPatterns        :: [Clause]
      -- ^ The set of patterns used as cover.
      , CoverResult -> IntSet
    coverNoExactClauses  :: IntSet -- Set Nat
      }